mathlib

33406172 - 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`.