English
Let R be an integral domain with enough roots of unity and n ≠ 0. For a in ZMod n, the sum of χ(a) over all Dirichlet characters χ mod n with values in R equals (n.totient) if a = 1, and 0 otherwise.
Русский
Пусть R — интегральное кольцо с достаточными корнями единства и n ≠ 0. Для каждого a в ZMod n сумма по χ(a) над всеми Dirichlet‑символами χ mod n с значениями в R равна (n.totient) при a = 1 и 0 в противном случае.
LaTeX
$$$\forall R\ [CommRing\ R]\ {n : \mathbb{N}}\ [NeZero\ n]\ [HasEnoughRootsOfUnity\ R (Monoid.exponent (ZMod n)ˣ)]\ [IsDomain\ R] (a : ZMod n), \sum χ : DirichletCharacter R n, χ a = \mathrm{ite} (a = 1) (n.totient : R) 0$$$
Lean4
/-- If `R` is an integral domain that has enough roots of unity and `n ≠ 0`, then
for `a` in `ZMod n`, the sum of `χ a` over all Dirichlet characters mod `n`
with values in `R` vanishes if `a ≠ 1` and has the value `n.totient` if `a = 1`. -/
theorem sum_characters_eq (a : ZMod n) : ∑ χ : DirichletCharacter R n, χ a = if a = 1 then (n.totient : R) else 0 :=
by
split_ifs with ha
·
simpa only [ha, map_one, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one,
← Nat.card_eq_fintype_card] using congrArg Nat.cast <| card_eq_totient_of_hasEnoughRootsOfUnity R n
· exact sum_characters_eq_zero R ha
