mathlib3

76ab749e - feat(analysis/normed_space/operator_norm): variants of continuous_linear_map.lsmul and their properties (#8984)