English
For χ ≠ 1, J(χ, χ^{-1}) = −χ(−1).
Русский
Для χ ≠ 1, J(χ, χ^{-1}) = −χ(−1).
LaTeX
$$$$ J(χ, χ^{-1}) = -χ(-1) $$$$
Lean4
/-- If `χ` is a nontrivial multiplicative character on a finite field `F`,
then `J(χ,χ⁻¹) = -χ(-1)`. -/
theorem jacobiSum_nontrivial_inv {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum χ χ⁻¹ = -χ (-1) := by
classical
rw [jacobiSum]
conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
have : ∑ x ∈ univ \ { 1 }, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x :=
by
refine
sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun x hx ↦ ?_)
(fun y hy ↦ ?_) (fun _ _ ↦ rfl)
· simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
rw [div_eq_iff <| sub_ne_zero.mpr ((ne_eq ..).symm ▸ hx).symm, mul_sub, mul_one, neg_one_mul, sub_neg_eq_add,
right_eq_add, neg_eq_zero]
exact one_ne_zero
· simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
exact one_ne_zero
· simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
rw [eq_comm, ← sub_eq_zero] at hx
simp [field]
· simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
simp [field]
rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
exact MulChar.sum_eq_zero_of_ne_one hχ
