mathlib

0a5f69cc - feat(src/order/basic): show injectivity of order conversions, and tag lemmas with ext (#6490)

feat(src/order/basic): show injectivity of order conversions, and tag lemmas with ext (#6490) Stating these as `function.injective` provides slightly more API, especially since before only the composition was proven as injective. For convenience, this leaves behind `preorder.ext`, `partial_order.ext`, and `linear_order.ext`, although these are now provable with trivial applications of `ext`.