Commit 2023-02-11 20:54 8374b993

View on Github →

feat: port GroupTheory.GroupAction.Quotient (#2213)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/Quotient.lean

added theorem MulAction.Quotient.coe_smul_out'

added theorem MulAction.Quotient.mk_smul_out'

added theorem MulAction.Quotient.smul_coe

added theorem MulAction.Quotient.smul_mk

added theorem MulAction.card_eq_sum_card_group_div_card_stabilizer'

added theorem MulAction.card_eq_sum_card_group_div_card_stabilizer

added theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group

added theorem MulAction.injective_ofQuotientStabilizer

added def MulAction.ofQuotientStabilizer

added theorem MulAction.ofQuotientStabilizer_mem_orbit

added theorem MulAction.ofQuotientStabilizer_mk

added theorem MulAction.ofQuotientStabilizer_smul

added theorem MulAction.orbitEquivQuotientStabilizer_symm_apply

added theorem MulAction.stabilizer_quotient

added theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group

added def MulActionHom.toQuotient

added theorem MulActionHom.toQuotient_apply

added theorem QuotientGroup.out'_conj_pow_minimalPeriod_mem

added theorem Subgroup.normalCore_eq_ker

added theorem Subgroup.quotientCenterEmbedding_apply

added theorem Subgroup.quotientCentralizerEmbedding_apply