English
Let G be a finite subgroup of the units of a ring. Then the sum of all elements of G, considered in the ring, equals 1 if G is the trivial subgroup and 0 otherwise.
Русский
Пусть G — конечная подгруппа единиц кольца. Тогда сумма всех элементов G в кольце равна 1, если G тривиальна, и нулю в противном случае.
LaTeX
$$$\sum_{x \in G} x = \begin{cases} 1, & G = \bot \\ 0, & \text{else} \end{cases}$$$
Lean4
/-- The sum of a subgroup of the units of a field is 1 if the subgroup is trivial and 1 otherwise -/
@[simp]
theorem sum_subgroup_units [Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] [Decidable (G = ⊥)] :
∑ x : G, (x.val : K) = if G = ⊥ then 1 else 0 :=
by
by_cases G_bot : G = ⊥
· subst G_bot
simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]
rw [Set.default_coe_singleton]
rfl
· simp only [G_bot, ite_false]
exact sum_subgroup_units_eq_zero G_bot
