Commit 2022-10-15 13:04 583cae77
View on Github →chore(analysis/normed_space/operator_norm): fix naming of continuous_linear_map.lmul
and similar (#15968)
This renames the continuous linear (bilinear) map given by multiplication in a non-unital algebra to match the non-continuous version (linear_map.mul
). The changes are as follows:
continuous_linear_map.lmul
→continuous_linear_map.mul
(the "l" was for "linear", which is redundant)continuous_linear_map.lmul_right
is deleted. This is literally just thecontinuous_linear_map.flip
of the map in (1) above. It's only use in mathlib is to define the map in (3) below, and creating it as a separate def seems unnecessary (and actively obscures the.flip
)continuous_linear_map.lmul_left_right
→continuous_linear_map.mul_left_right
. This matcheslinear_map.mul_left_right
(although the latter is uncurried). Docstrings have also been updated, both to reflect the non-unital generalization from #15868, but also because the old docstrings mentioned "left multiplication", but this should just be called "multiplication".