mathlib

fb22ae33 - refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150)

refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150) This means that we can talk about `rel_iso` without needing to transitively import `ordered_group`s This PR takes advantage of this to define `order_iso.mul_(left|right)[']` to mirror `equiv.mul_(left|right)[']`.