theorem Hex.NumberTower.Norm.quadratic_resultant (a b p q : ℂ) : (Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C a).resultant (Polynomial.C p + Polynomial.C q * Polynomial.X) 2 1 = p * p - b * p * q + a * q * q

The quadratic norm identity, with formal degrees so the linear coefficient may vanish.

theorem Hex.NumberTower.Norm.quadratic_congr (a b p q : ℂ) (g : Polynomial ℂ) (n : ℕ) (hn : g.natDegree ≤ n) (heval : ∀ (z : ℂ), z * z + b * z + a = 0 → Polynomial.eval z g = p + q * z) : (Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C a).resultant g 2 n = p * p - b * p * q + a * q * q

Replacing a polynomial by a linear expression with the same values on the roots of a monic quadratic preserves its resultant, including repeated roots and a vanishing linear coefficient.

@[instance_reducible]

noncomputable def Hex.NumberTower.Norm.instCommRingDensePoly_hexNumberFieldTowerMathlib {R : Type u_1} [CommRing R] [DecidableEq R] : CommRing (DensePoly R)

Equations

• Hex.NumberTower.Norm.instCommRingDensePoly_hexNumberFieldTowerMathlib = Hex.NumberTower.Norm.denseCommRing

@[instance_reducible]

noncomputable def Hex.NumberTower.Norm.instCommRingDensePoly_hexNumberFieldTowerMathlib_1 {R : Type u_1} [Field R] [DecidableEq R] : CommRing (DensePoly R)

Equations

• Hex.NumberTower.Norm.instCommRingDensePoly_hexNumberFieldTowerMathlib_1 = Hex.NumberTower.Norm.denseCommRing

theorem Hex.NumberTower.Norm.quadratic_eq_resultant (level : Level) (lower : List Level) (hdegree : level.degree = 2) (hlower : LevelsValid lower) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (f : Array (Array ℚ)) (c : ℤ) : quadratic level lower f c = Array.map Arithmetic.Coeff.data ((definingOuter level lower).resultant (shiftedOuter level lower f c)).toArray

The bounded quadratic computation returns exactly the encoded resultant. Only the lower tower must be a field; the top quadratic may have repeated roots or a nonzero linear coefficient.

theorem Hex.NumberTower.Norm.oneLevel_eq (level : Level) (lower : List Level) (hlower : LevelsValid lower) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (f : Array (Array ℚ)) (c : ℤ) : oneLevel level lower f c = Array.map Arithmetic.Coeff.data ((definingOuter level lower).resultant (shiftedOuter level lower f c)).toArray

The quadratic dispatch and the general fallback compute the same encoded one-level resultant over every validated lower tower.