Commit 2020-08-15 17:58 050728b0
View on Github →feat(data/fintype/basic): card lemma and finset bool alg (#3796) Adds the card lemma
finset.card_le_univ [fintype α] (s : finset α) : s.card ≤ fintype.card α
which I expected to see in mathlib, and upgrade the bounded_distrib_lattice instance on finset in the presence of fintype to a boolean algebra instance.