Theorems · Theorem · number theory

gaussSum_mulShift

∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
  (ψ : AddChar R R') (a : Rˣ), χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ

Replacing ψ by mulShift ψ a and multiplying the Gauss sum by χ a does not change it.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingFintypeCommRing