Odd-degree norm curves keep their degree and irreducibility in every residue characteristic, including characteristic two. The signs ±1 remain nonzero in every field.

theorem CCDN.signedNormCurvePolynomial_map_irreducible_in_every_characteristic (K : Type u_1) (E : Type u_2) [Field K] [NumberField K] [Field E] (β : NumberField.RingOfIntegers K) {ε : ℤ} (hε : ↑ε ≠ 0) (hn : Odd (Module.finrank ℚ K)) : Irreducible ((MvPolynomial.map (Int.castRingHom E)) (signedNormCurvePolynomial K β ε))

If [K : ℚ] is odd and the sign ε is nonzero in the field E, then the signed norm-curve polynomial of β remains irreducible over E, in any characteristic.

theorem CCDN.signedNormCurvePolynomial_map_totalDegree (K : Type u_1) (E : Type u_2) [Field K] [NumberField K] [Field E] (β : NumberField.RingOfIntegers K) {ε : ℤ} (hε : ↑ε ≠ 0) (hn : 2 ≤ Module.finrank ℚ K) : ((MvPolynomial.map (Int.castRingHom E)) (signedNormCurvePolynomial K β ε)).totalDegree = Module.finrank ℚ K

If [K : ℚ] ≥ 2 and the sign ε is nonzero in the field E, then the signed norm-curve polynomial of β has total degree [K : ℚ] over E.