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
.