mathlib
159d9aca - split(order/max): Split off `order.basic` (#11603)

Commit

3 years ago

split(order/max): Split off `order.basic` (#11603) This moves `is_bot`, `is_top`, `no_min_order`, `no_max_order` to a new file `order.max`.

Author

YaelDillies

Parents