Theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group

Modification history

2023-11-01 10:38
Mathlib/GroupTheory/GroupAction/Quotient.lean
refactor(GroupTheory/GroupAction/Basic): re-organise, rename, and make some variables implicit (#7786) …
Modified MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_groupView on Github →
2023-02-11 20:54
Mathlib/GroupTheory/GroupAction/Quotient.lean
feat: port GroupTheory.GroupAction.Quotient (#2213)
Added MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_groupView on Github →