mathlib3

2b9ab3bb - split(data/psigma/order): Split off `order.lexicographic` (#10953)

split(data/psigma/order): Split off `order.lexicographic` (#10953) This moves all the stuff about `Σ' i, α i` to a new file `data.psigma.order`. This mimics the file organisation of `sigma`. I'm crediting: * Scott for #820 * Minchao for #914