Commit 2023-07-01 17:13 d055df48

View on Github →

feat: port Geometry.Manifold.DerivationBundle (#5640)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/DerivationBundle.lean

added def Derivation.evalAt

added theorem Derivation.evalAt_apply

added def PointDerivation

added def PointedSmoothMap.eval

added theorem PointedSmoothMap.smul_def

added def PointedSmoothMap

added def SmoothFunction.evalAt

added theorem apply_fdifferential

added theorem apply_hfdifferential

added def fdifferential

added theorem fdifferential_comp

added def hfdifferential