Theorems · Theorem · number theory

gaussSum_mul_gaussSum_eq_card

∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'}, χ ≠ 1 → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)

We have gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R when χ is nontrivial and ψ is primitive (and R is a field).

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFintypeCommRingIsDomain