English
If χ is nontrivial and ψ is primitive, then gaussSum χ ψ · gaussSum χ⁻¹ ψ⁻¹ = card R.
Русский
Если χ не тривиален и ψ примитивна, то gaussSum χ ψ · gaussSum χ⁻¹ ψ⁻¹ =card R.
LaTeX
$$$\mathrm{gaussSum}(χ, ψ) \cdot \mathrm{gaussSum}(χ^{-1}, ψ^{-1}) = |R|$$$
Lean4
/-- We have `gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R`
when `χ` is nontrivial and `ψ` is primitive (and `R` is a field). -/
theorem gaussSum_mul_gaussSum_eq_card {χ : MulChar R R'} (hχ : χ ≠ 1) {ψ : AddChar R R'} (hψ : IsPrimitive ψ) :
gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R :=
by
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']
conv =>
enter [1, 2, x, 2, y]
rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
-- conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
simp_rw [gaussSum_mul_aux hχ ψ]
rw [Finset.sum_comm]
classical -- to get `[DecidableEq R]` for `sum_mulShift`
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
simp only [Finset.mem_univ, map_one, one_mul, if_true]
