Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 22:52 8c0b8c71

View on Github →

feat(group_theory/subgroup/basic): Contrapositive of card_le_one_iff_eq_bot (#9918) Adds contrapositive of card_le_one_iff_eq_bot.

Estimated changes