mathlib3

b2a5f0d6 - feat(analysis/schwartz_space): construction of continuous linear maps (#18651)

feat(analysis/schwartz_space): construction of continuous linear maps (#18651) This PR has two parts: (a) create two definitions to construct continuous linear maps (the point being that one wants to reuse the boundedness estimate for both the well-posedness and the continuity) and (b) drastically reduce the boilerplate for `schwartz_map.fderiv_clm`.