Generator_of_Normal_Subgroup
Provedconjugationgroup-theorynormal-closureproofwiki
The normal closure of a set S in a group G is closed under conjugation.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Generator_of_Normal_Subgroup {G : Type _} [Group G] (S : Set G) : ∀ (g : G), ∀ s ∈ Subgroup.normalClosure S, g * s * g⁻¹ ∈ Subgroup.normalClosure S := by sorrySource