The full odd-degree norm polynomial gives an absolutely irreducible double-cover equation. No squarefree-part substitution is made.

theorem CCDN.odd_degree_double_cover_irreducible {F : Type u_1} [Field F] (p : Polynomial F) (hp : Odd p.natDegree) : Irreducible (Polynomial.X ^ 2 - Polynomial.C p)

For a polynomial p of odd degree over a field F, the double-cover polynomial Y ^ 2 - p is irreducible in F[X][Y].

theorem CCDN.double_cover_bivariateTotalDegree {R : Type u_1} [CommRing R] (p : Polynomial R) (hp : 2 ≤ p.natDegree) : bivariateTotalDegree (Polynomial.X ^ 2 - Polynomial.C p) = p.natDegree

For a polynomial p of degree at least 2, the double-cover polynomial Y ^ 2 - p has total degree deg p.

theorem CCDN.signedNormCurvePolynomial_totalDegree (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) {ε : ℤ} (hε : ε ≠ 0) (hn : 2 ≤ Module.finrank ℚ K) : (signedNormCurvePolynomial K β ε).totalDegree = Module.finrank ℚ K

For [K : ℚ] ≥ 2 and ε ≠ 0, the signed norm-curve polynomial y ^ 2 - ε * N(x - β) has total degree [K : ℚ].