Subset_has_2_Conjugates_then_Normal_Subgroup
Provedconjugationgroup-theorynormal-subgroupproofwiki
If a subgroup H of G has exactly two conjugates, then G has a proper non-trivial normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Subset_has_2_Conjugates_then_Normal_Subgroup {G : Type _} [Group G] (H : Subgroup G) (h : H.normalizer.index = 2) : ∃ N : Subgroup G, N.Normal ∧ N ≠ ⊥ ∧ N ≠ ⊤ := by sorrySource