mathlib3
8b913902
- feat(order/hom/basic): add `order_iso.with_{top,bot}_congr` (#12264)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(order/hom/basic): add `order_iso.with_{top,bot}_congr` (#12264) This adds: * `with_bot.to_dual_top` * `with_top.to_dual_bot` * `order_iso.with_top_congr` * `order_iso.with_bot_congr`
Author
eric-wieser
Parents
2840532e
Loading