Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-14 04:30 c8c18697

View on Github →

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

Estimated changes

Modified src/algebra/ordered_group.lean

Modified src/analysis/convex/cone.lean

Modified src/data/fin.lean

Modified src/data/real/nnreal.lean

Modified src/geometry/manifold/manifold.lean

Modified src/group_theory/subgroup.lean

Modified src/group_theory/submonoid.lean

Modified src/linear_algebra/basic.lean

Modified src/order/basic.lean

modified def decidable_linear_order.lift

modified def linear_order.lift

modified def partial_order.lift

modified def preorder.lift

Modified src/order/zorn.lean

Modified src/ring_theory/subsemiring.lean

Modified src/topology/algebra/open_subgroup.lean