mathlib3

eb3595ed - move(order/*): move from `algebra.order.` the files that aren't about algebra (#9562)

move(order/*): move from `algebra.order.` the files that aren't about algebra (#9562) `algebra.order.basic` and `algebra.order.functions` never mention `+`, `-` or `*`. Thus they belong under `order`.