mathlib3

234b3df2 - feat(analysis/normed_space): lemmas about continuous bilinear maps (#13522)

feat(analysis/normed_space): lemmas about continuous bilinear maps (#13522) * Define `continuous_linear_map.map_sub₂` and friends, similar to the lemmas for `linear_map`. * Rename `continuous_linear_map.map_add₂` to `continuous_linear_map.map_add_add` * Two comments refer to `continuous.comp₂`, which will be added in #13423 (but there is otherwise no dependency on this PR). * Define `precompR` and `precompL`, which will be used to compute the derivative of a convolution. * From the sphere eversion project * Required for convolutions