Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-18 22:20 0b673ed4

View on Github →

feat(set_theory/cardinal/ordinal): cardinality of α →₀ β (#15198) As requested by @YaelDillies.

Estimated changes

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.mk_finsupp_lift_of_fintype

added theorem cardinal.mk_finsupp_of_fintype

Modified src/set_theory/cardinal/ordinal.lean

added theorem cardinal.mk_finsupp_lift_of_infinite

added theorem cardinal.mk_finsupp_of_infinite

modified theorem cardinal.mk_list_eq_mk