Theorem tangentMapWithin_snd

Modification history

2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified tangentMapWithin_sndView on Github →
2026-01-27 19:55
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: tangentMap(Within)_snd (#34369) …
Added tangentMapWithin_sndView on Github →