English
If χ has order n and ψ is primitive, then gaussSum χ ψ · gaussSum χ^{n-1} ψ = χ(-1) · card R.
Русский
Если χ имеет порядок n и ψ примитивна, то gaussSum χ ψ · gaussSum χ^{n-1} ψ = χ(-1) · card R.
LaTeX
$$$\mathrm{gaussSum}(χ, ψ) \cdot \mathrm{gaussSum}(χ^{n-1}, ψ) = χ(-1) \cdot |R|, \quad n=\mathrm{order}(χ)$$$
Lean4
/-- If `χ` is a multiplicative character of order `n` on a finite field `F`,
then `g(χ) * g(χ^(n-1)) = χ(-1)*#F` -/
theorem gaussSum_mul_gaussSum_pow_orderOf_sub_one {χ : MulChar R R'} {ψ : AddChar R R'} (hχ : χ ≠ 1)
(hψ : ψ.IsPrimitive) : gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * Fintype.card R :=
by
have h : χ ^ (orderOf χ - 1) = χ⁻¹ :=
by
refine (inv_eq_of_mul_eq_one_right ?_).symm
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]
rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ, MulChar.inv_apply',
inv_neg_one]
