Number_of_Distinct_Conjugate_Subsets_is_Index_of_Normalizer_v4
Provedconjugationgroup-theoryindexnormalizerproofwiki
The number of distinct conjugates of a subgroup H in G equals the index of the normalizer of H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Number_of_Distinct_Conjugate_Subsets_is_Index_of_Normalizer_v4 {G : Type _} [Group G] (H : Subgroup G) : Nat.card {K : Subgroup G | ∃ g : G, K = H.map (MulAut.conj g).toMonoidHom} = H.normalizer.index := by sorrySource