Commit 2022-08-07 16:31 a6b56ec2

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.