Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 14:29 234b3df2

View on Github →

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

Estimated changes