Commit 2021-10-22 15:58 20bb02f6
View on Github →feat(data/fintype/basic): fintype.card_pos (#9876)
Two lemmas fintype.card_pos and fintype.card_ne_zero that are often easier to use than fintype.card_pos_iff.
feat(data/fintype/basic): fintype.card_pos (#9876)
Two lemmas fintype.card_pos and fintype.card_ne_zero that are often easier to use than fintype.card_pos_iff.