mathlib

773b45f7 - feat(algebra/module/ordered): redefine `ordered_module` as `ordered_smul` (#8930)

feat(algebra/module/ordered): redefine `ordered_module` as `ordered_smul` (#8930) One would like to talk about `ordered_monoid R (with_top R)`, but the `module` constraint is too strict to allow this. The definition of `ordered_monoid` works if it is loosened to `has_scalar R M`. Most of the proofs that are part of its API need at most `smul_with_zero`. So it has been loosened to `smul_with_zero`, since a lawless `ordered_monoid` wouldn't do much. In the `ordered_field` portion, `module` has been loosened to `mul_action_with_zero`. `order_dual` instances of `smul` instances have also been generalized to better transmit. There are more generalizations possible, but seem out of scope for a single PR. Unfortunately, these generalizations exposed a gnarly misalignment between `prod.has_lt` and `prod.has_le`, which have incompatible definitions, when inferred through separate paths. In particular, the `lt` definition of generated by `prod.preorder` is different than the core `prod.has_lt`. Due to this, the `prod.ordered_monoid` instance has not been generalized. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>