Theorems · Theorem · number theory

gaussSum_mul

∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ φ : MulChar R R')
  (ψ : AddChar R R'), gaussSum χ ψ * gaussSum φ ψ = ∑ t, ∑ x, χ x * φ (t - x) * ψ t

A formula for the product of two Gauss sums with the same additive character.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFintypeCommRing