Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-02 06:39 50583b9e

View on Github →

feat(algebra/order): additional theorems on cmp

Estimated changes

Modified algebra/order.lean

added theorem cmp_compares

added theorem cmp_swap

added theorem ordering.or_else_eq_lt

added theorem ordering.swap_or_else

Modified order/basic.lean

added def decidable_linear_order.lift