Commit 2020-06-29 12:45 36ce13fe

View on Github →

chore(finset/nat/antidiagonal): simplify some proofs (#3225) Replace some proofs with rfl, and avoid multiset.to_finset when there is a nodup available.

Estimated changes

Modified src/data/finset.lean

added theorem finset.card_mk

Modified src/data/list/antidiagonal.lean

Modified src/data/multiset.lean