mathlib3
0190177e - feat(group_theory/subgroup): eq_top_of_le_card and eq_bot_of_card_le (#8414)

Commit

4 years ago

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`.

Author

tb65536

Parents

d8fc0817

mathlib3 0190177e - feat(group_theory/subgroup): eq_top_of_le_card and eq_bot_of_card_le (#8414)

mathlib3
0190177e - feat(group_theory/subgroup): eq_top_of_le_card and eq_bot_of_card_le (#8414)