A consequence of Burnside's lemma

See Mathlib.GroupTheory.GroupAction.Quotient for Burnside's lemma itself. This lemma is separate because it requires Nat.card and hence transitively the development of cardinals.

theorem card_comm_eq_card_conjClasses_mul_card (G : Type u_1) [Group G] : Nat.card { p : G × G // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G