Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.lift_mk_eq'

Modification history

2021-08-24 04:00
src/set_theory/cardinal.lean
feat(linear_algebra/dimension): generalize dim_map_le to heterogeneous universes (#8800) …
Added cardinal.lift_mk_eq'View on Github →