Mathlib v3 is deprecated. Go to Mathlib v4

Def partial_order_of_SO

Modification history

2021-09-14 15:08
src/order/rel_classes.lean
chore(order/pilex): use `*_order_of_*TO` from `order.rel_classes` (#9129) …
Modified partial_order_of_SOView on Github →
2020-06-14 12:37
src/order/basic.lean
chore(order/basic): move unbundled order classes to `rel_classes (#3066) …
Modified partial_order_of_SOView on Github →
2017-12-31 16:53
order/basic.lean
feat(data/ordinal): is_normal, omin, power/log, CNF, indecomposables, …
Added partial_order_of_SOView on Github →