feat(group_theory/subgroup): eq_bot_of_card_eq (#8413)
feat(group_theory/subgroup): eq_bot_of_card_eq (#8413)

Companion lemma to `eq_top_of_card_eq`.





leanprover-community/mathlib,leanprover-community/mathlib