mathlib3
afd8a525 - feat(order/hom/basic): add simp lemmas for `strict_mono.order_iso` and friends (#13606)

Commit
3 years ago
feat(order/hom/basic): add simp lemmas for `strict_mono.order_iso` and friends (#13606) Formalized as part of the Sphere Eversion project.
Author
Parents
Loading