basic): improve docs on `lift`, add `simp` lemmas (#14599)

Commit

3 years ago

feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599) This is pretty much the same thing as #14596, just on `ordinal.lift` instead of `cardinal.lift`.

Author

vihdzp

Parents

d0b93faf

mathlib d21469e4 - feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599)

mathlib
d21469e4 - feat(set_theory/ordinal/basic): improve docs on `lift`, add `simp` lemmas (#14599)