gaussSum_frob — Mathlib

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

Похожие утверждения