English
If every element of a set s has finite order, then the subgroup closure of s, viewed as a submonoid, equals the submonoid closure of s.
Русский
Если каждый элемент множества s имеет конечный порядок, то замыкание подгруппы s, взятое как подмоноид, равно замыканию подмоноида Closure s.
LaTeX
$$(closure s).toSubmonoid = Submonoid.closure s, given ∀ x ∈ s, IsOfFinOrder x$$
Lean4
/-- See `Subgroup.closure_toSubmonoid_of_finite` for a version for finite groups. -/
@[to_additive /-- See `AddSubgroup.closure_toAddSubmonoid_of_finite` for a version for finite additive groups. -/
]
theorem closure_toSubmonoid_of_isOfFinOrder {s : Set G} (hs : ∀ x ∈ s, IsOfFinOrder x) :
(closure s).toSubmonoid = Submonoid.closure s :=
by
refine le_antisymm ?_ (le_closure_toSubmonoid s)
rw [closure_toSubmonoid]
refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure fun x (hx : x⁻¹ ∈ s) ↦ ?_
apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)
simp [(hs _ hx).mem_powers_iff_mem_zpowers]
