English
For χ, ψ, χ(−1) · gaussSum χ ψ⁻¹ = gaussSum χ ψ.
Русский
Для χ, ψ выполняется χ(−1) · gaussSum χ ψ⁻¹ = gaussSum χ ψ.
LaTeX
$$$\chi(-1) \cdot \mathrm{gaussSum}(\chi, ψ^{-1}) = \mathrm{gaussSum}(\chi, ψ)$$$
Lean4
/-- For a quadratic character `χ` and when the characteristic `p` of the target ring
is a unit in the source ring, the `p`th power of the Gauss sum of`χ` and `ψ` is
`χ p` times the original Gauss sum. -/
theorem gaussSum_frob (hp : IsUnit (p : R)) {χ : MulChar R R'} (hχ : IsQuadratic χ) (ψ : AddChar R R') :
gaussSum χ ψ ^ p = χ p * gaussSum χ ψ := by
rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit, ← mul_assoc, hp.unit_spec, ←
pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec, one_apply_coe, one_mul]
