Commit 2021-11-15 19:11 1a47cfc7

View on Github →

feat(data/finset/basic): A finset has card two iff it's {x, y} for some x ≠ y (#10252) and the similar result for card three. Dumb but surprisingly annoying!

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.card_eq_three

added theorem finset.card_eq_two

Modified src/data/list/basic.lean

added theorem list.length_eq_three

added theorem list.length_eq_two

Modified src/data/multiset/basic.lean

added theorem multiset.card_eq_three

added theorem multiset.card_eq_two