Commit 2021-09-20 04:23 976b261a

View on Github →

feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185) A generic theorem about the cardinality of a finset or multiset with an element erased.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.card_erase_eq_ite

modified theorem finset.erase_empty

Modified src/data/multiset/basic.lean

added theorem multiset.card_erase_eq_ite