Normalizer_of_Subgroup_is_Largest_Subgroup_containing_that_Subgroup_as_Normal_Subgroup
Provednormal-subgroupsnormalizersproofwiki
The normalizer of H is the largest subgroup containing H as a normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Normalizer_of_Subgroup_is_Largest_Subgroup_containing_that_Subgroup_as_Normal_Subgroup {G : Type _} [Group G] (H : Subgroup G) : H ≤ H.normalizer := by sorrySource