English
If p is a prime in the target ring and χ is quadratic, then gaussSum χ ψ^p = χ(p) gaussSum χ ψ (Frobenius compatibility).
Русский
Если p — простое в целевом кольце и χ квадратичен, то gaussSum χ ψ^p = χ(p) gaussSum χ ψ (совместимость с Фробениусом).
LaTeX
$$$\mathrm{gaussSum}(χ, ψ)^p = χ(p) \cdot \mathrm{gaussSum}(χ, ψ)$$$
Lean4
/-- When `χ` is a nontrivial quadratic character, then the square of `gaussSum χ ψ`
is `χ(-1)` times the cardinality of `R`. -/
theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : χ ≠ 1) (hχ₂ : IsQuadratic χ) {ψ : AddChar R R'} (hψ : IsPrimitive ψ) :
gaussSum χ ψ ^ 2 = χ (-1) * Fintype.card R :=
by
rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']
congr
rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mulShift]
rfl
