mathlib

632b4970 - feat(analysis/inner_product/calculus): [higher] differentiability to/from `euclidean_space` (#15363)

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 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>