English
Let R be an integral domain with enough roots of unity and n ≠ 0. For a unit a ∈ ZMod n and any b ∈ ZMod n, the sum over χ of χ(a⁻¹) χ(b) equals n.totient if a = b, and 0 otherwise.
Русский
Пусть R — интегральное кольцо с корнями единства и n ≠ 0. Для единицы a ∈ ZMod n и любого b ∈ ZMod n сумма по χ χ(a⁻¹) χ(b) равна n.totient если a = b, иначе 0.
LaTeX
$$$\forall R\ [CommRing\ R]\ {n : \mathbb{N}}\ [NeZero\ n]\ [HasEnoughRootsOfUnity\ R (Monoid.exponent (ZMod n)ˣ)]\ [IsDomain\ R] {a : ZMod n} (ha : IsUnit a) (b : ZMod n), \
\sum χ : DirichletCharacter R n, χ a⁻¹ * χ b = \text{ite } (a = b) (n.totient : R) 0$$$
Lean4
/-- 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`. -/
theorem sum_char_inv_mul_char_eq {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then (n.totient : R) else 0 := by
simp only [← map_mul, sum_characters_eq, ZMod.inv_mul_eq_one_of_isUnit ha]
