mathlib3
465508fc - split(order/monotone): split off `order.basic` (#9518)

Commit

4 years ago

split(order/monotone): split off `order.basic` (#9518)

Author

YaelDillies

YaelDillies

Parents

Loading