Theorems · Theorem · number theory

DirichletCharacter.sum_characters_eq_zero

∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [inst_3 : IsDomain R] ⦃a : ZMod n⦄, a ≠ 1 → ∑ χ, χ a = 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for each a ≠ 1 in ZMod n, the sum of χ a over all Dirichlet characters mod n with values in R vanishes.

Defined in

Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingNeZeroHasEnoughRootsOfUnityIsDomain