BoundedSMul over normed additive groups #
Lemmas which hold only in
NormedSpace α β are provided in another file.
Notably we prove that
NonUnitalSeminormedRings have bounded actions by left- and right-
multiplication. This allows downstream files to write general results about
BoundedSMul, and then
mul_const results as an immediate corollary.