English
For a quadratic χ and primitive ψ, gaussSum χ ψ ^ p = χ p · gaussSum χ ψ.
Русский
Для квадратичного χ и примитивного ψ, gaussSum χ ψ ^ p = χ p · gaussSum χ ψ.
LaTeX
$$$\mathrm{gaussSum}(χ, ψ)^p = χ(p) \cdot \mathrm{gaussSum}(χ, ψ)$$$
Lean4
/-- For a quadratic character `χ` and when the characteristic `p` of the target ring
is a unit in the source ring and `n` is a natural number, the `p^n`th power of the Gauss
sum of`χ` and `ψ` is `χ (p^n)` times the original Gauss sum. -/
theorem gaussSum_frob_iter (n : ℕ) (hp : IsUnit (p : R)) {χ : MulChar R R'} (hχ : IsQuadratic χ) (ψ : AddChar R R') :
gaussSum χ ψ ^ p ^ n = χ ((p : R) ^ n) * gaussSum χ ψ := by
induction n with
| zero => rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
| succ n ih =>
rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul, ←
pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]
