Commit 2026-09-22 12:37 5837ec1d

View on Github →

feat(GroupTheory/Index): add Lagrange's theorem for monoid homomorphisms (#43845)

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

modified theorem Subgroup.card_dvd_of_surjective

added theorem Subgroup.card_ker_mul_card_of_surjective

added theorem Subgroup.card_ker_mul_card_range

modified theorem Subgroup.index_map_dvd

modified theorem Subgroup.index_map_of_injective

Modified Mathlib/GroupTheory/Schreier.lean