Order_of_Conjugate_of_Subgroup_v3
Provedconjugationgroup-theoryorderproofwikisubgroup
Let G be a group and H a subgroup. Then for any a in G, the conjugate aHa⁻¹ has the same cardinality as H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Conjugate_of_Subgroup_v3 {G : Type _} [Group G] (H : Subgroup G) (a : G) : Nat.card (H.map (MulAut.conj a).toMonoidHom) = Nat.card H := by sorrySource