feat(algebra/order/smul): `positivity` extension for `smul` (#16162)
feat(algebra/order/smul): `positivity` extension for `smul` (#16162)

Add `positivity_smul`, a `positivity` extension to deal with `•`.





leanprover-community/mathlib,leanprover-community/mathlib