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

Conjugate decomposition

Decomposes sums into Frobenius-conjugate classes in the extension-field argument of Carlitz (1969).

noncomputable def KloostermanWeil.Carlitz.conjSigmaEquiv (F : Type u_1) (L : Type u_2) [Field F] [Field L] [Algebra F L] : (c : ConjRootClass F L) × ↑c.carrier ≃ L

Partition an algebra extension into its conjugacy classes over the base field.

Equations

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

theorem KloostermanWeil.Carlitz.sum_eq_sum_conjRootClass {F : Type u_1} {L : Type u_2} {M : Type u_3} [Field F] [Field L] [Algebra F L] [Fintype L] [Fintype (ConjRootClass F L)] [(c : ConjRootClass F L) → Fintype ↑c.carrier] [AddCommMonoid M] (f : L → M) : ∑ x : L, f x = ∑ c : ConjRootClass F L, ∑ x : ↑c.carrier, f ↑x