Commit 2023-08-09 17:44 f1e12780

View on Github →

refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier (#6290) This PR moves a formula for the number of conjugacy classes earlier. The proof uses Burnside's theorem, so it cannot be moved any earlier than GroupTheory/GroupAction/Quotient.

Estimated changes

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/GroupTheory/CommutingProbability.lean

deleted theorem card_comm_eq_card_conjClasses_mul_card

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

added theorem card_comm_eq_card_conjClasses_mul_card