Commit 2026-06-15 11:33 dd9f867f

View on Github →

feat: custom elaborators for TangentSpace and tangentMap(Within) (#36155) And use these to golf the differential geometry files a bit further.

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/GroupLieAlgebra.lean

modified theorem mulInvariantVectorField_eq_mpullback

Modified Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

modified def IsMIntegralCurve

modified def IsMIntegralCurveAt

modified def IsMIntegralCurveOn

Modified Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

modified theorem mfderiv_id

modified theorem mfderiv_prod_eq_add_apply

modified theorem tangentMap_id

Modified Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean

Modified Mathlib/Geometry/Manifold/Notation.lean

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

modified theorem enorm_tangentSpace_vectorSpace

modified theorem nnnorm_tangentSpace_vectorSpace

modified theorem norm_tangentSpace_vectorSpace

modified def normedSpaceTangentSpaceVectorSpace

Modified Mathlib/Geometry/Manifold/Riemannian/PathELength.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified MathlibTest/DifferentialGeometry/Notation/Basic.lean