Theorems · Theorem · number theory

MulChar.IsQuadratic.gaussSum_frob

∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
  [fp : Fact (Nat.Prime p)] [hch : CharP R' p],
  IsUnit ↑p → ∀ {χ : MulChar R R'}, χ.IsQuadratic → ∀ (ψ : AddChar R R'), gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ

For a quadratic character χ and when the characteristic p of the target ring is a unit in the source ring, the pth power of the Gauss sum of χ and ψ is χ p times the original Gauss sum.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

1 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFintypeCommRingFactCharP