Mathlib v3 is deprecated. Go to Mathlib v4

Def preorder.lift

Modification history

2021-06-09 15:40
src/order/basic.lean
fix(*): make some non-instances reducible (#7835) …
Modified preorder.liftView on Github →
2020-06-14 04:30
src/order/basic.lean
refactor(order/basic): make `*order.lift` use `[]` argument (#3067) …
Modified preorder.liftView on Github →
2019-05-08 22:40
src/order/basic.lean
refactor(order/basic): make type class args explicit in {*}order.lift (#995) …
Modified preorder.liftView on Github →
2018-09-07 17:30
order/basic.lean
refactor(linear_algebra, ring_theory): rework submodules; move them to linear_algebra
Added preorder.liftView on Github →