English
Let K be a finite field and i a natural number with i < q − 1. Then the sum of x^i over all x ∈ K equals 0.
Русский
Пусть K — конечное поле, и i < q−1. Тогда сумма x^i по всем x ∈ K равна нулю.
LaTeX
$$$\sum_{x \in K} x^i = 0$ when $i < q-1$$$
Lean4
/-- The sum of `x ^ i` as `x` ranges over a finite field of cardinality `q`
is equal to `0` if `i < q - 1`. -/
theorem sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) : ∑ x : K, x ^ i = 0 :=
by
by_cases hi : i = 0
· simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]
classical
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.val_injective⟩
have : univ.map φ = univ \ {0} := by
ext x
simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff, mem_singleton, φ] using
isUnit_iff_ne_zero
calc
∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
_ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
_ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq
