Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 12:27 aa812bd1

View on Github →

chore(group_theory/group_action/basic): split file (#15044) Split the file group_theory/group_action/basic to remove the dependency on group_theory/quotient_group, moving everything involving quotients to a new file group_theory/group_action/quotient.

Estimated changes

Modified src/algebra/polynomial/group_ring_action.lean

Modified src/category_theory/action.lean

Modified src/data/zmod/quotient.lean

Modified src/group_theory/commuting_probability.lean

Modified src/group_theory/complement.lean

Modified src/group_theory/group_action/basic.lean

deleted theorem mul_action.card_eq_sum_card_group_div_card_stabilizer'

deleted theorem mul_action.card_eq_sum_card_group_div_card_stabilizer

deleted theorem mul_action.card_orbit_mul_card_stabilizer_eq_card_group

deleted theorem mul_action.injective_of_quotient_stabilizer

deleted def mul_action.of_quotient_stabilizer

deleted theorem mul_action.of_quotient_stabilizer_mem_orbit

deleted theorem mul_action.of_quotient_stabilizer_mk

deleted theorem mul_action.of_quotient_stabilizer_smul

deleted theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply

deleted theorem mul_action.quotient.coe_smul_out'

deleted theorem mul_action.quotient.mk_smul_out'

deleted theorem mul_action.quotient.smul_coe

deleted theorem mul_action.quotient.smul_mk

deleted theorem mul_action.stabilizer_quotient

deleted theorem mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group

deleted def mul_action_hom.to_quotient

deleted theorem mul_action_hom.to_quotient_apply

deleted theorem subgroup.normal_core_eq_ker

Created src/group_theory/group_action/quotient.lean

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 theorem mul_action.injective_of_quotient_stabilizer

added def mul_action.of_quotient_stabilizer

added theorem mul_action.of_quotient_stabilizer_mem_orbit

added theorem mul_action.of_quotient_stabilizer_mk

added theorem mul_action.of_quotient_stabilizer_smul

added theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply

added theorem mul_action.quotient.coe_smul_out'

added theorem mul_action.quotient.mk_smul_out'

added theorem mul_action.quotient.smul_coe

added theorem mul_action.quotient.smul_mk

added theorem mul_action.stabilizer_quotient

added theorem mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group

added def mul_action_hom.to_quotient

added theorem mul_action_hom.to_quotient_apply

added theorem subgroup.normal_core_eq_ker

Modified src/group_theory/p_group.lean

Modified src/linear_algebra/alternating.lean

Modified src/linear_algebra/quotient.lean

Modified src/topology/algebra/group.lean