Commit 2022-05-03 14:29 234b3df2

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