mathlib3

583cae77 - chore(analysis/normed_space/operator_norm): fix naming of `continuous_linear_map.lmul` and similar (#15968)

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".