smul): `positivity` extension for `smul` (#16162)

Commit

3 years ago

feat(algebra/order/smul): `positivity` extension for `smul` (#16162) Add `positivity_smul`, a `positivity` extension to deal with `•`.

Author

YaelDillies

Parents