Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-24 22:55 02b37b5a

View on Github →

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

Estimated changes