Commit 2021-09-08 16:06 f4f1cd3f

feat(algebra/module/ordered): simple smul lemmas (#9077) These are the negative versions of the lemmas in ordered_smul, which suggests that both files should be merged. Note however that, contrary to those, they need module k M instead of merely smul_with_zero k M.