Theorems · Theorem · number theory

gaussSum_mulShift_eq

∀ {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ˣ), gaussSum χ (ψ.mulShift ↑a) = χ⁻¹ ↑a * gaussSum χ ψ

Replacing ψ by mulShift ψ a multiplies the Gauss sum by χ⁻¹ a.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFintypeCommRing