Commit 2020-06-10 07:15 6a0412e9

View on Github →

chore(data/fintype): generalise to_finset_card (#2316) Slight generalisation of a lemma, allowing a more flexible fintype instance. Also americanises some spelling. :-)

Estimated changes

Modified archive/imo1988_q6.lean

Modified archive/sensitivity.lean

Modified src/data/equiv/basic.lean

Modified src/data/fintype/basic.lean

added theorem set.to_finset_card

Modified src/data/set/finite.lean

deleted theorem set.to_finset_card

modified theorem set.to_finset_inter