mathlib
c8c18697 - refactor(order/basic): make `*order.lift` use `[]` argument (#3067)

Commit

6 years ago

refactor(order/basic): make `*order.lift` use `[]` argument (#3067) Take an order on the codomain as a `[*order β]` argument.

Author

urkud

Parents