Theorem injective_fderivWithin_writtenInExtChartAt

Modification history

2026-11-10 17:26
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: `isInvertible_fderivWithin_writtenInExtChartAt` (#44843) …
Added injective_fderivWithin_writtenInExtChartAtView on Github →