English
Let α be a finite abelian group (viewed additively). The sum of the complex-valued characters ψ of α, evaluated at any element a ∈ α, equals |α| when a = 0 and equals 0 when a ≠ 0. In symbols, ∑_{ψ} ψ(a) = (|α|) if a = 0, and 0 otherwise.
Русский
Пусть α — конечная абелева группа под сложением. Сумма значений всех символьных функций ψ на α, взятых в точке a ∈ α, равна |α|, если a = 0, и равна 0, если a ≠ 0. Обозначим сумму как ∑_{ψ} ψ(a).
LaTeX
$$$$ \\sum_{\\psi \\in \\mathrm{AddChar}(\\alpha, \\mathbb{C})} \\psi(a) \\;=\\; \\begin{cases} |\\alpha|, & a = 0 \\\\\\ 0, & a \\neq 0 \\end{cases} \\quad \\text{(cast to } \\mathbb{C} \\text{ when needed)} $$$$
Lean4
theorem sum_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
∑ ψ : AddChar α ℂ, ψ a = if a = 0 then (Fintype.card α : ℂ) else 0 := by
simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)
