mathlib
01fa7f52 - feat(data/fintype/basic): `one_lt_card_iff` and `two_lt_card_iff` (#11524)

Commit
3 years ago
feat(data/fintype/basic): `one_lt_card_iff` and `two_lt_card_iff` (#11524) This PR adds `one_lt_card_iff` and `two_lt_card_iff`.
Author
Parents
Loading