Conjugate_of_Set_with_Inverse_is_Closed
Provedconjugationgroup-theorynormal-closureproofwiki
Let G be a group and S a subset. The normal closure of S equals the subgroup generated by all conjugates of elements in S ∪ S⁻¹.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Conjugate_of_Set_with_Inverse_is_Closed {G : Type _} [Group G] (S : Set G) : Subgroup.normalClosure S = Subgroup.closure {g * s * g⁻¹ | (g : G) (s : G) (_ : s ∈ S ∪ S⁻¹)} := by sorrySource