Commit 2024-12-20 11:33 5465191d

View on Github →

feat(GroupTheory/Index): Add Subgroup.card_range_dvd and Subgroup.card_map_dvd (#20100) This PR adds a few missing lemmas to GroupTheory/Index.lean.

Estimated changes

added theorem Subgroup.card_map_dvd