English
Jacobi sum equals a sum over univ minus {0,1}: J(χ, ψ) = ∑_{x ∈ univ \ {0,1}} χ(x) ψ(1−x).
Русский
Сумма Якоби равна сумме по всем x кроме 0 и 1: J(χ, ψ) = ∑_{x ∈ univ \ {0,1}} χ(x) ψ(1−x).
LaTeX
$$$$ J(\chi, \psi) = \sum_{x \in \mathrm{univ} \setminus \{0,1\}} \chi(x) \psi(1 - x). $$$$
Lean4
/-- The Jacobi sum of two multiplicative characters on a nontrivial finite commutative ring `F`
can be written as a sum over `F \ {0,1}`. -/
theorem jacobiSum_eq_sum_sdiff (χ ψ : MulChar F R) : jacobiSum χ ψ = ∑ x ∈ univ \ {0, 1}, χ x * ψ (1 - x) :=
by
simp only [jacobiSum, subset_univ, sum_sdiff_eq_sub, sub_eq_add_neg, left_eq_add, neg_eq_zero]
apply sum_eq_zero
simp only [mem_insert, mem_singleton, forall_eq_or_imp, χ.map_zero, neg_zero, add_zero, map_one, mul_one, forall_eq,
add_neg_cancel, ψ.map_zero, mul_zero, and_self]
