English
Let R be an integral domain that has enough roots of unity and n ≠ 0. For any a ≠ 1 in ZMod n, the sum over all Dirichlet characters χ mod n with values in R satisfies ∑ χ χ(a) = 0.
Русский
Пусть R — интегральное кольцо и обладает достаточным количеством корней единицы, и n ≠ 0. Для любого a ≠ 1 в ZMod n сумма по всем Dirichlet‑символам χ mod n с значениями в R равна 0.
LaTeX
$$$\forall R\ [CommRing\ R]\ {n : \mathbb{N}}\ [NeZero\ n]\ [HasEnoughRootsOfUnity\ R (Monoid.exponent (ZMod n)ˣ)]\ [IsDomain\ R], \forall ⦃a : ZMod n⦄, a \neq 1 \Rightarrow \sum χ : DirichletCharacter R n, χ a = 0$$$
Lean4
/-- 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. -/
theorem sum_characters_eq_zero ⦃a : ZMod n⦄ (ha : a ≠ 1) : ∑ χ : DirichletCharacter R n, χ a = 0 :=
by
obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha
refine eq_zero_of_mul_eq_self_left hχ ?_
simp only [Finset.mul_sum, ← MulChar.mul_apply]
exact Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl
