Commit 2021-12-15 19:58 3f55e027
View on Github →feat(data/{multiset, finset}/basic): add card_mono (#10771)
Add a @[mono] lemma for finset.card. Also multiset.card_mono as an alias of a preexisting lemma.
feat(data/{multiset, finset}/basic): add card_mono (#10771)
Add a @[mono] lemma for finset.card. Also multiset.card_mono as an alias of a preexisting lemma.