Number_of_Conjugates_is_Number_of_Cosets_of_Centralizer
Provedcentralizerconjugationgroup-theoryindexproofwiki
The number of distinct conjugates of a in G equals the number of cosets of the centralizer of a, i.e., [G : C_G(a)].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Number_of_Conjugates_is_Number_of_Cosets_of_Centralizer {G : Type _} [Group G] (a : G) : Nat.card (MulAction.orbit (ConjAct G) a) = (Subgroup.centralizer ({a} : Set G)).index := by sorrySource