basic): Contrapositive of `card_le_one_iff_eq_bot` (#9918)

Commit

4 years ago

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

Author

tb65536

Parents