English
For χ quadratic and ψ primitive, gaussSum χ ψ^{p^n} = χ(p^n) gaussSum χ ψ.
Русский
Для квадратичного χ и примитивного ψ, gaussSum χ ψ^{p^n} = χ(p^n) gaussSum χ ψ.
LaTeX
$$$\mathrm{gaussSum}(χ, ψ)^{p^n} = χ(p^n) \cdot \mathrm{gaussSum}(χ, ψ)$$$
Lean4
/-- When `R'` has prime characteristic `p`, then the `p`th power of the Gauss sum
of `χ` and `ψ` is the Gauss sum of `χ^p` and `ψ^p`. -/
theorem gaussSum_frob (χ : MulChar R R') (ψ : AddChar R R') : gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p) :=
by
rw [← frobenius_def, gaussSum, gaussSum, map_sum]
simp_rw [pow_apply' χ fp.1.ne_zero, map_mul, frobenius_def]
rfl