English
If χ ≠ 1, then J(1, χ) = −1.
Русский
Если χ ≠ 1, то J(1, χ) = −1.
LaTeX
$$$$ J(1, \chi) = -1 \quad (\chi \neq 1). $$$$
Lean4
/-- If `χ` is a nontrivial multiplicative character on a finite field `F`, then `J(1,χ) = -1`. -/
theorem jacobiSum_one_nontrivial {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum 1 χ = -1 := by
classical
have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 :=
by
apply Finset.sum_eq_zero
simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← isUnit_iff_ne_zero, true_and,
MulChar.one_apply, sub_self, zero_mul, implies_true]
simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ, add_zero,
Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one, sub_add_cancel_left, this]
