mathlib3

2ca1b571 - chore(algebra/order/{module, smul}): Move to the correct spot (#16131)

chore(algebra/order/{module, smul}): Move to the correct spot (#16131) Make `algebra.order.module` do what it says on the tin. Namely, move everything that wasn't about `module` to `algebra.order.smul` and generalize accordingly. As a bonus, add a shortcut instance for `ordered_smul 𝕜 (ι → 𝕜)` as this solves #16021.