BoundedSMul hypotheses

Stream: mathlib4

[Jireh Loreaux]

Why is BoundedSMul defined for PseudoMetricSpace and not Bornology? Is it just that it never got refactored?

[Jireh Loreaux]

This came up because I realized we have no BoundedMul.to_boundedSMul instance, which I thought should exist trivially.

[Jireh Loreaux]

And because of the definition of BoundedSMul, the best we have is docs#NonUnitalSeminormedRing.to_boundedSMul