English
For a nontrivial finite subgroup G of the units of a field K, the sum of its elements (viewed in K) is zero: ∑_{x∈G} x = 0.
Русский
Для недобитой конечной подгруппы G единиц поля K сумма её элементов в полях равна нулю: ∑_{x∈G} x = 0.
LaTeX
$$$\sum_{x \in G} x = 0$$$
Lean4
/-- The sum of a nontrivial subgroup of the units of a field is zero. -/
theorem sum_subgroup_units_eq_zero [Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [Fintype G] (hg : G ≠ ⊥) :
∑ x : G, (x.val : K) = 0 := by
rw [Subgroup.ne_bot_iff_exists_ne_one] at hg
rcases hg with
⟨a, ha⟩
-- The action of a on G as an embedding
let a_mul_emb : G ↪ G := mulLeftEmbedding a
have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by
simp
-- Therefore the sum of x over a G is the sum of a x over G
have h_sum_map :=
Finset.univ.sum_map a_mul_emb fun x =>
((x : Kˣ) : K)
-- ... and the former is the sum of x over G.
-- By algebraic manipulation, we have Σ G, x = ∑ G, a x = a ∑ G, x
simp only [h_unchanged, mulLeftEmbedding_apply, Subgroup.coe_mul, Units.val_mul, ← mul_sum, a_mul_emb] at h_sum_map
have hzero : (((a : Kˣ) : K) - 1) = 0 ∨ ∑ x : ↥G, ((x : Kˣ) : K) = 0 := by
rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
apply Or.resolve_left hzero
contrapose! ha
ext
rwa [← sub_eq_zero]
