Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-27 12:20 133067cf

View on Github →

feat(set_theory/cardinal_ordinal): cardinal.mk_finset_eq_mk (#3578)

Estimated changes

Modified src/data/finset/basic.lean

added theorem list.to_finset_surjective

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.mk_finset_eq_mk