English
If χ and ψ are the trivial multiplicative characters on a finite field F, then J(χ, ψ) = |F| − 2.
Русский
Если χ и ψ — тривиальные мультипликативные симметрические символы на конечном поле F, то J(χ, ψ) = |F| − 2.
LaTeX
$$$$ \mathrm{jacobiSum}(\mathrm{trivial}, \mathrm{trivial}) = |F| - 2. $$$$
Lean4
/-- The Jacobi sum of twice the trivial multiplicative character on a finite field `F`
equals `#F-2`. -/
theorem jacobiSum_trivial_trivial : jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = Fintype.card F - 2 := by
classical
rw [jacobiSum_eq_sum_sdiff]
have : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1 :=
by
intro x hx
rw [← map_mul, MulChar.trivial_apply, if_pos]
simp only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← ne_eq, true_and] at hx
simpa only [isUnit_iff_ne_zero, mul_ne_zero_iff, ne_eq, sub_eq_zero, @eq_comm _ _ x] using hx
calc
∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x)
_ = ∑ _ ∈ univ \ {0, 1}, 1 := (sum_congr rfl this)
_ = #(univ \ {0, 1}) := (cast_card _).symm
_ = Fintype.card F - 2 := by
rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]
