mathlib

158fbc5d - refactor(algebra/module/order): Make space argument explicit in the `order_iso` (#9706)

refactor(algebra/module/order): Make space argument explicit in the `order_iso` (#9706) Explicitly providing `M` in `order_iso.smul_left` and `order_iso.smul_left_dual` turns out to work much better with dot notation on `order_iso`. This allows golfing half the proofs introduced in #9078.