Commit 2026-01-27 19:55 98d411ac

View on Github →

feat: tangentMap(Within)_snd (#34369) From fpvandoorn and my LeanCourse25.

Estimated changes

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

added theorem tangentMapWithin_snd

added theorem tangentMap_snd