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.

instance instInfiniteProdSubtypeCommute {α : Type u_1} [Mul α] [Infinite α] : Infinite { p : α × α // Commute p.1 p.2 }

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