Commit 2021-09-06 12:25 773b45f7

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.