Commit 2022-08-25 00:16 2ca1b571
View on Github →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.