Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes