Commit 2026-06-23 15:06 247b7ec2

View on Github →

doc: fix the doc of two files about group actions (#40138)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

modified theorem MulAction.Quotient.coe_smul_out

modified theorem MulAction.Quotient.mk_smul_out

modified theorem MulAction.Quotient.smul_coe

modified theorem MulAction.Quotient.smul_mk

modified theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group

modified theorem MulAction.coe_quotient_smul

modified theorem MulAction.injective_ofQuotientStabilizer

modified def MulAction.ofQuotientStabilizer

modified theorem MulAction.ofQuotientStabilizer_mem_orbit

modified theorem MulAction.ofQuotientStabilizer_mk

modified theorem MulAction.ofQuotientStabilizer_smul

modified theorem MulAction.orbitEquivQuotientStabilizer_symm_apply

modified theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group

modified def MulActionHom.toQuotient

modified theorem MulActionHom.toQuotient_apply

modified theorem QuotientGroup.out_conj_pow_minimalPeriod_mem

Modified Mathlib/GroupTheory/Schreier.lean