Commit 2022-08-07 16:31 a6b56ec2
View on Github →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.