Normal_Subgroup_iff_Normalizer_is_Group
Provednormal-subgroupsnormalizersproofwiki
H is normal in G iff the normalizer of H equals G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Normal_Subgroup_iff_Normalizer_is_Group {G : Type _} [Group G] (H : Subgroup G) : H.Normal ↔ H.normalizer = ⊤ := by sorrySource
Human review