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

Irreducibles in the generating identity

Organizes the irreducible polynomial factors that contribute to the Carlitz (1969) generating-series construction.

def KloostermanWeil.Carlitz.RelevantIrred (p n : ℕ) [Fact (Nat.Prime p)] : Type

Monic irreducibles whose degree divides the extension degree.

Equations

• KloostermanWeil.Carlitz.RelevantIrred p n = { P : Polynomial (KloostermanWeil.Carlitz.Fp p) // P.Monic ∧ Irreducible P ∧ P.natDegree ∣ n }

noncomputable def KloostermanWeil.Carlitz.classToRelevant (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (c : ConjRootClass (Fp p) (Ext p n)) : RelevantIrred p n

Associate to a conjugacy class its monic irreducible minimal polynomial.

Equations

• KloostermanWeil.Carlitz.classToRelevant p n c = ⟨c.minpoly, ⋯⟩

theorem KloostermanWeil.Carlitz.classToRelevant_injective (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] : Function.Injective (classToRelevant p n)

theorem KloostermanWeil.Carlitz.classToRelevant_surjective (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] : Function.Surjective (classToRelevant p n)

noncomputable def KloostermanWeil.Carlitz.classRelevantEquiv (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] : ConjRootClass (Fp p) (Ext p n) ≃ RelevantIrred p n

Conjugacy classes in a finite extension parametrized by relevant irreducibles.

Equations

• KloostermanWeil.Carlitz.classRelevantEquiv p n = Equiv.ofBijective (KloostermanWeil.Carlitz.classToRelevant p n) ⋯