Commit 2022-10-08 20:02 619fd4d5

View on Github →

feat(data/finite/card): Add finite.card_pos (#16858) We already have finite.card_pos_iff analogous to fintype.card_pos_iff. This PR adds finite.card_pos analogous to fintype.card_pos.

Estimated changes

Modified src/data/finite/card.lean

added theorem finite.card_pos

modified theorem finite.card_pos_iff