Elementary inputs

Three bookkeeping inputs the assembled theorem needs:

• a primitive additive character K → ℂ is supplied by Mathlib (KasamiCyclicAdditive.primitiveAddChar);
• the exponent inverse D is supplied by the extended Euclidean algorithm;
• the admissible-slope finset is nonempty as soon as |K| > 2.

theorem KasamiCyclicAdditive.exists_inverse_exponent {m N : ℕ} (hcop : m.Coprime N) (hN : 1 < N) : ∃ (D : ℕ), D ≠ 0 ∧ m * D ≡ 1 [MOD N]

Coprimality yields a nonzero inverse exponent D with m * D ≡ 1 [MOD N]. The modulus is abstract; the application takes N = |Kˣ|.

theorem KasamiCyclicAdditive.slopes_nonempty_of_two_lt_card {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (hcard : 2 < Fintype.card K) : (slopes K).Nonempty

A finite field with more than two elements has an admissible slope.

theorem KasamiCyclicAdditive.slopes_nonempty_of_card_two_pow {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) : (slopes K).Nonempty

The field-cardinality hypothesis occurring in the Kasami statement implies nonempty slopes as soon as 2 ≤ n.