mathlib

a6b56ec2 - refactor(analysis/normed_space/operator_norm): generalize `continuous_linear_map.lmul` to non-unital algebras (#15868)

refactor(analysis/normed_space/operator_norm): generalize `continuous_linear_map.lmul` to non-unital algebras (#15868) After the recent refactor in #15310 of `algebra.lmul` (resulting in `linear_map.mul` in particular) the type class restrictions on `continuous_linear_map.lmul` (and `continuous_linear_map.lmul_right` and `continuous_linear_map.lmul_right_left`) can be weakened to non-unital normed algebras, which we do here. `continuous_linear_map.lmulₗᵢ` and `continuous_linear_map.lmul_rightₗᵢ` have not had their type class requirements weakened because they require `norm_one_class`, and hence unital algebras. In many non-unital algebras (including all non-unital normed algebras with an approximate unit, and hence all C⋆-algebras), the maps `continuous_linear_map.lmul` (and `lmul_right`) are nevertheless isometric, but this requires other properties so they are not implemented here.