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

Coefficients of monic polynomials

Equivalences between coefficient vectors and monic polynomials used in the Carlitz factorization. The coefficient algebra is proved here.

noncomputable def KloostermanWeil.Carlitz.coeffVectorToMonic (p n : ℕ) [Fact (Nat.Prime p)] : (Fin n → ZMod p) → MonicDeg p n

Adjoin a leading coefficient of one to a vector of lower coefficients.

Equations

• KloostermanWeil.Carlitz.coeffVectorToMonic p n a = ⟨KloostermanWeil.Dickson.monicFromCoeffs p n a, ⋯⟩

noncomputable def KloostermanWeil.Carlitz.monicToCoeffVector (p n : ℕ) : MonicDeg p n → Fin n → ZMod p

Extract the coefficients below the leading term of a monic polynomial.

Equations

• KloostermanWeil.Carlitz.monicToCoeffVector p n f i = (Polynomial.coeff ↑f) ↑i

theorem KloostermanWeil.Carlitz.coeffVector_left_inv (p n : ℕ) [Fact (Nat.Prime p)] (a : Fin n → ZMod p) : monicToCoeffVector p n (coeffVectorToMonic p n a) = a

theorem KloostermanWeil.Carlitz.coeffVector_right_inv (p n : ℕ) [Fact (Nat.Prime p)] (f : MonicDeg p n) : coeffVectorToMonic p n (monicToCoeffVector p n f) = f

noncomputable def KloostermanWeil.Carlitz.coeffVectorEquivMonicDeg (p n : ℕ) [Fact (Nat.Prime p)] : (Fin n → ZMod p) ≃ MonicDeg p n

Monic degree-n polynomials parametrized by their n lower coefficients.

Equations

• One or more equations did not get rendered due to their size.