Commit 2022-06-15 00:05 7b2970fa

View on Github →

feat(set_theory/cardinal/basic): improve docs on lift, add simp lemmas (#14596) We add some much needed documentation to the cardinal.lift API. We also mark a few extra lemmas with simp.

Estimated changes

Modified src/set_theory/cardinal/basic.lean

modified theorem cardinal.lift_id'

modified theorem cardinal.lift_umax'

modified theorem cardinal.lift_umax