Commit 2021-07-26 15:58 0190177e

View on Github →

feat(group_theory/subgroup): eq_top_of_le_card and eq_bot_of_card_le (#8414) Slight strengthenings of the lemmas eq_top_of_card_eq and eq_bot_of_card_eq.

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.eq_bot_of_card_le

added theorem subgroup.eq_top_of_le_card