Commit 2022-07-19 03:29 632b4970

feat(analysis/inner_product/calculus): [higher] differentiability to/from euclidean_space (#15363) This duplicates some of the calculus pi API to euclidean_space. Namely :

• we duplicate all the variants of differentiable_pi to show that a function to a euclidean space is (higher) differentiable iff all of its components are
• we introduce euclidean_version.proj, analogous to continuous_linear_map.proj. This allows us to avoid duplicating all the differentiable_apply-like lemmas, because one can just use the API for smoothness of continuous linear maps