mathlib
02b37b5a - feat(group_theory/subgroup): eq_bot_of_card_eq (#8413)

Commit

4 years ago

feat(group_theory/subgroup): eq_bot_of_card_eq (#8413) Companion lemma to `eq_top_of_card_eq`.

Author

tb65536

Parents