mathlib

6d2788c2 - feat(analysis/calculus/cont_diff): cont_diff_succ_iff_fderiv_apply (#13797)

feat(analysis/calculus/cont_diff): cont_diff_succ_iff_fderiv_apply (#13797) * Prove that a map is `C^(n+1)` iff it is differentiable and all its directional derivatives in all points are `C^n`. * Also some supporting lemmas about `continuous_linear_equiv`. * We only manage to prove this when the domain is finite dimensional. * Prove one direction of `cont_diff_on_succ_iff_fderiv_within` with fewer assumptions * From the sphere eversion project Co-authored by: Patrick Massot [patrick.massot@u-psud.fr](mailto:patrick.massot@u-psud.fr) Co-authored by: Oliver Nash [github@olivernash.org](mailto:github@olivernash.org)