feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538)
feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538)

* From the sphere eversion project
* Required for convolutions





leanprover-community/mathlib,leanprover-community/mathlib