mathlib3
090e59d0 - feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538)

Commit
3 years ago
feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538) * From the sphere eversion project * Required for convolutions
Author
Parents
Loading