Theorem mfderivWithin_neg

Modification history

2026-06-19 13:16
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat(Geometry/Manifold/Notation): add (d)elaborators for `UniqueMDiffOn` and `UniqueMDiffWithinAt` (#40748) …
Modified mfderivWithin_negView on Github →
2026-05-31 10:14
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat: add `mvfderivWithin` with (d)elaborators and basic API (#39513) …
Modified mfderivWithin_negView on Github →
2026-05-16 15:19
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat: mfderivWithin_{add,neg,sub} (#39451) …
Added mfderivWithin_negView on Github →