English
If every pair of elements of a set k commutes, then the subgroup closure of k is a commutative (abelian) group.
Русский
Если любые две элементы множества k commute, то порожденная этим множесто подгруппа является абелевой.
LaTeX
$$$\operatorname{CommGroup}(\mathrm{closure}(k))$$$
Lean4
/-- If all the elements of a set `s` commute, then `closure s` is a commutative group. -/
@[to_additive /-- If all the elements of a set `s` commute, then `closure s` is an additive commutative group. -/
]
abbrev closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : CommGroup (closure k) :=
{ (closure k).toGroup with
mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
have := closure_le_centralizer_centralizer k
Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
