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

Monic factorization data

Encodes monic polynomial factorizations as finite data for Carlitz-type generating identities (Carlitz 1969).

@[reducible, inline]

abbrev KloostermanWeil.Carlitz.FpPoly (p : ℕ) : Type

Polynomials over the prime residue ring.

Equations

• KloostermanWeil.Carlitz.FpPoly p = Polynomial (ZMod p)

def KloostermanWeil.Carlitz.MonicDeg (p n : ℕ) : Type

Monic polynomials of the specified natural degree.

Equations

• KloostermanWeil.Carlitz.MonicDeg p n = { f : KloostermanWeil.Carlitz.FpPoly p // Polynomial.Monic f ∧ Polynomial.natDegree f = n }

def KloostermanWeil.Carlitz.FactorData (p n : ℕ) : Type

Multisets of monic irreducibles whose degrees sum to the specified total degree.

Equations

• KloostermanWeil.Carlitz.FactorData p n = { s : Multiset (KloostermanWeil.Carlitz.FpPoly p) // (∀ q ∈ s, Irreducible q ∧ Polynomial.Monic q) ∧ (Multiset.map Polynomial.natDegree s).sum = n }

noncomputable def KloostermanWeil.Carlitz.factorDataOf (p n : ℕ) [Fact (Nat.Prime p)] : MonicDeg p n → FactorData p n

The normalized irreducible factor multiset of a monic polynomial.

Equations

• KloostermanWeil.Carlitz.factorDataOf p n f = ⟨UniqueFactorizationMonoid.normalizedFactors ↑f, ⋯⟩

noncomputable def KloostermanWeil.Carlitz.monicDegOfFactorData (p n : ℕ) [Fact (Nat.Prime p)] : FactorData p n → MonicDeg p n

Reconstruct a monic polynomial by multiplying its irreducible factor data.

Equations

• KloostermanWeil.Carlitz.monicDegOfFactorData p n s = ⟨(↑s).prod, ⋯⟩

theorem KloostermanWeil.Carlitz.factorData_left_inv (p n : ℕ) [Fact (Nat.Prime p)] (f : MonicDeg p n) : monicDegOfFactorData p n (factorDataOf p n f) = f

theorem KloostermanWeil.Carlitz.factorData_right_inv (p n : ℕ) [Fact (Nat.Prime p)] (s : FactorData p n) : factorDataOf p n (monicDegOfFactorData p n s) = s

noncomputable def KloostermanWeil.Carlitz.monicFactorEquiv (p n : ℕ) [Fact (Nat.Prime p)] : MonicDeg p n ≃ FactorData p n

Unique factorization as an equivalence between monic polynomials and factor data.

Equations

• KloostermanWeil.Carlitz.monicFactorEquiv p n = { toFun := KloostermanWeil.Carlitz.factorDataOf p n, invFun := KloostermanWeil.Carlitz.monicDegOfFactorData p n, left_inv := ⋯, right_inv := ⋯ }