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

Trace characters of polynomial classes

Relates extension-field trace characters to values on polynomial classes. The underlying construction follows Carlitz (1969).

theorem KloostermanWeil.Carlitz.trace_carlitz_arg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : K) {x : L} (hx : x ≠ 0) : (Algebra.trace K L) (x + (algebraMap K L) t * x⁻¹) = ↑(Module.finrank (↥K⟮x⟯) L) * (-(minpoly K x).nextCoeff - t * ((minpoly K x).coeff 1 / (minpoly K x).coeff 0))

theorem KloostermanWeil.Carlitz.psiExt_carlitz_arg_eq_etaPoly_pow (p n : ℕ) [Fact (Nat.Prime p)] (t : Fp p) {x : Ext p n} (hx : x ≠ 0) : (psiExt p n) (x + (algebraMap (Fp p) (Ext p n)) t * x⁻¹) = Dickson.etaPoly p t (minpoly (Fp p) x) ^ Module.finrank (↥(Fp p)⟮x⟯) (Ext p n)