mathlib3

63c0dac6 - refactor(module/ordered): make ordered_semimodule a mixin (#4719)

refactor(module/ordered): make ordered_semimodule a mixin (#4719) Per @urkud's suggestion at #4683. This should avoid having to introduce a separate `ordered_algebra` class. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>