Commit 2022-08-31 11:42 eaa51e72

View on Github →

feat(algebra/order/smul): ordered_smul instances for ℕ and ℤ (#16247) A linear ordered monoid/group has ordered scalar multiplication by ℕ/ℤ.

Estimated changes

Modified src/algebra/order/smul.lean

added theorem ordered_smul.mk''

Modified test/positivity.lean