Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-02 19:07 d821860f

View on Github →

feat(group_theory/group_action/basic): class formula, Burnside's lemma (#8801) This adds class formula and Burnside's lemma for group action, both as an equiv and using cardinals. I also added a cardinal version of the Orbit-stabilizer theorem.

Estimated changes

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified src/data/equiv/basic.lean

added def equiv.sigma_assoc

Modified src/group_theory/group_action/basic.lean

added theorem add_action.stabilizer_vadd_eq_stabilizer_map_conj

added theorem mul_action.card_eq_sum_card_group_div_card_stabilizer'

added theorem mul_action.card_eq_sum_card_group_div_card_stabilizer

added theorem mul_action.card_orbit_mul_card_stabilizer_eq_card_group

added def mul_action.self_equiv_sigma_orbits'

added theorem mul_action.stabilizer_smul_eq_stabilizer_map_conj

added theorem mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group

Modified src/group_theory/subgroup.lean

added def mul_equiv.subgroup_equiv_map

Modified src/group_theory/submonoid/operations.lean

added def mul_equiv.submonoid_equiv_map