Smallest_Normal_Subgroup_containing_Set
Provedgroup-theorynormal-closurenormal-subgroupproofwiki
For any subset S of a group G, there exists a unique smallest normal subgroup of G containing S.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Smallest_Normal_Subgroup_containing_Set {G : Type _} [Group G] (S : Set G) : ∃ N : Subgroup G, N.Normal ∧ S ⊆ N ∧ ∀ K : Subgroup G, K.Normal → S ⊆ K → N ≤ K := by sorrySource