smul): `ordered_smul` instances for `ℕ` and `ℤ` (#16247)

Commit

3 years ago

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

Author

YaelDillies

Parents

f951e201

mathlib eaa51e72 - feat(algebra/order/smul): `ordered_smul` instances for `ℕ` and `ℤ` (#16247)

mathlib
eaa51e72 - feat(algebra/order/smul): `ordered_smul` instances for `ℕ` and `ℤ` (#16247)