English
For a finite group G and a monoid hom f: G → R, the sum over G of f equals card(G) if f is trivial, otherwise 0.
Русский
Для конечной группы G и гомоморфизма f: G → R сумма по G равна |G| если f тривиальна, иначе 0.
LaTeX
$$$\text{Let } f:G\to R \text{ with decidable } (f=1).\; \sum_{g\in G} f(g)=\begin{cases}|G|,& f=1; \\ 0,& \text{else}.\end{cases}$$$
Lean4
/-- In an integral domain, a sum indexed by a homomorphism from a finite group is zero,
unless the homomorphism is trivial, in which case the sum is equal to the cardinality of the group.
-/
theorem sum_hom_units (f : G →* R) [Decidable (f = 1)] : ∑ g : G, f g = if f = 1 then Fintype.card G else 0 :=
by
split_ifs with h
· simp [h]
· rw [Nat.cast_zero]
exact sum_hom_units_eq_zero f h
