Commit 2022-10-15 13:04 583cae77

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:

1. continuous_linear_map.lmul → continuous_linear_map.mul (the "l" was for "linear", which is redundant)
2. continuous_linear_map.lmul_right is deleted. This is literally just the continuous_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)
3. continuous_linear_map.lmul_left_right → continuous_linear_map.mul_left_right. This matches linear_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".