Commit 2023-08-14 12:56 c54060b4

View on Github →

feat: the class equation (groups) (#6375) This is mostly mathported work of Johan's towards Wedderburn's Little theorem.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_set_coe

Created Mathlib/GroupTheory/ClassEquation.lean

added theorem Group.card_center_add_sum_card_noncenter_eq_card

added theorem Group.nat_card_center_add_sum_card_noncenter_eq_card

added theorem Group.sum_card_conj_classes_eq_card

added theorem sum_conjClasses_card_eq_card

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

added theorem ConjAct.orbit_eq_carrier_conjClasses

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

added theorem ConjClasses.card_carrier

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem ConjClasses.mem_noncenter

added theorem ConjClasses.mk_bijOn

added def ConjClasses.noncenter