feat(operator_norm): smul_right lemmas (#4150)
from the sphere eversion project
We need a version of `continuous_linear_map.smul_right` that is itself a continuous linear map from a normed space to a space of continuous linear maps.
breaking changes:
* rename `smul_right_norm` to `norm_smul_right_apply`
* in `homothety_norm` remove useless sign assumption and switch from assuming positive dimension to `nontrivial`
