mathlib
6a6b0a56 - chore(order/pilex): use `_order_of_TO` from `order.rel_classes` (#9129)

Commit

4 years ago

chore(order/pilex): use `*_order_of_*TO` from `order.rel_classes` (#9129) This changes definitional equality for `≤` on `pilex` from `x < y ∨ x = y` to `x = y ∨ x < y`.

Author

urkud

Parents

91f053e1

mathlib 6a6b0a56 - chore(order/pilex): use `*_order_of_*TO` from `order.rel_classes` (#9129)

mathlib
6a6b0a56 - chore(order/pilex): use `_order_of_TO` from `order.rel_classes` (#9129)