Set_of_Words_Generates_Group
Provedgeneratorsgroup-theoryproofwikiwords
Let S be a subset of a group G. Let S_hat = S ∪ S⁻¹. Then the subgroup generated by S equals the subgroup generated by S_hat.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Set_of_Words_Generates_Group {G : Type _} [Group G] (S : Set G) : Subgroup.closure S = Subgroup.closure (S ∪ S⁻¹) := by sorrySource