Theorems · Theorem · number theory

DirichletCharacter.sum_char_inv_mul_char_eq

∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [inst_3 : IsDomain R] {a : ZMod n}, IsUnit a → ∀ (b : ZMod n), ∑ χ, χ a⁻¹ * χ b = if a = b then ↑n.totient else 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for a and b in ZMod n with a a unit, the sum of χ a⁻¹ * χ b over all Dirichlet characters mod n with values in R vanishes if a ≠ b and has the value n.totient if a = b.

Defined in

Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingNeZeroHasEnoughRootsOfUnityIsDomain