Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Minimal polynomials and inverse sums

Minimal-polynomial identities used to express inverse terms in extension-field Kloosterman sums (Carlitz 1969).

theorem KloostermanWeil.Carlitz.minpoly_coeff_zero_ne_zero_of_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} (hx : x ≠ 0) : (minpoly K x).coeff 0 ≠ 0

theorem KloostermanWeil.Carlitz.adjoin_inv_eq_adjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} : K⟮x⁻¹⟯ = K⟮x⟯

theorem KloostermanWeil.Carlitz.minpoly_inv_natDegree_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} : (minpoly K x⁻¹).natDegree = (minpoly K x).natDegree

noncomputable def KloostermanWeil.Carlitz.invMinpolyCandidate (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (x : L) : Polynomial K

The reciprocal minimal polynomial normalized using its constant coefficient.

Equations

• KloostermanWeil.Carlitz.invMinpolyCandidate K L x = Polynomial.C ((minpoly K x).coeff 0)⁻¹ * (minpoly K x).reverse

theorem KloostermanWeil.Carlitz.invMinpolyCandidate_monic {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} (hx : x ≠ 0) : (invMinpolyCandidate K L x).Monic

theorem KloostermanWeil.Carlitz.invMinpolyCandidate_aeval_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} (hx : x ≠ 0) : (Polynomial.aeval x⁻¹) (invMinpolyCandidate K L x) = 0

theorem KloostermanWeil.Carlitz.invMinpolyCandidate_natDegree {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} (hx : x ≠ 0) : (invMinpolyCandidate K L x).natDegree = (minpoly K x).natDegree

theorem KloostermanWeil.Carlitz.minpoly_inv_eq_normalized_reverse {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} (hx : x ≠ 0) : minpoly K x⁻¹ = invMinpolyCandidate K L x

theorem KloostermanWeil.Carlitz.reverse_nextCoeff_eq_coeff_one {K : Type u_1} [Field K] {P : Polynomial K} (hdeg : 0 < P.natDegree) (hc : P.coeff 0 ≠ 0) : P.reverse.nextCoeff = P.coeff 1

theorem KloostermanWeil.Carlitz.minpoly_inv_nextCoeff_eq_coeff_one_div_coeff_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {x : L} (hx : x ≠ 0) : (minpoly K x⁻¹).nextCoeff = (minpoly K x).coeff 1 / (minpoly K x).coeff 0