feat(algebra/bounds): `smul` of upper/lower bounds (#9078)
feat(algebra/bounds): `smul` of upper/lower bounds (#9078)

This relates `lower_bounds (a • s)`/`upper_bounds (a • s)` and `a • lower_bounds s`/`a • upper_bounds s`.





leanprover-community/mathlib,leanprover-community/mathlib