Commit 2020-03-29 05:46 5d9e7f58

feat(analysis/calculus/fderiv): define has_strict_fderiv_at (#2249)

• Move code aroud
• general constructions (product, chain rule) before arithmetic;
• bundled E →L[𝕜] F maps before unbundled
• Use maps_to instead of f '' _ ⊆ _
• feat(analysis/calculus/fderiv): define has_strict_fderiv_at Prove strict differentiability of all functions found in this file, cleanup.
• Update src/analysis/calculus/fderiv.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
• Docs, var name