Size_of_Conjugacy_Class_is_Index_of_Centralizer_v2
Provedcentralizerconjugacy-classgroup-theoryindexproofwiki
The size of the conjugacy class of x in G equals the index of the centralizer of x in G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Size_of_Conjugacy_Class_is_Index_of_Centralizer_v2 {G : Type _} [Group G] (x : G) : Nat.card (MulAction.orbit (ConjAct G) x) = (Subgroup.centralizer ({x} : Set G)).index := by sorrySource