Def order_hom.unique
Modification history
2022-08-16 10:36
src/order/hom/basic.lean
chore(*): restore `subsingleton` instances and remove hacks (#16046) …
Deleted order_hom.uniqueView on Github →2021-12-23 10:36
src/order/hom/basic.lean
chore(order/*): Change `order_hom` notation (#10988) …
Modified order_hom.uniqueView on Github →