Theorem mvfderivWithin_eq_fderivWithin

Modification history

2026-09-08 09:08
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: add `mvfderivWithin_eq_fderivWithin` and `mvfderiv_eq_fderiv` (#42443) …
Added mvfderivWithin_eq_fderivWithinView on Github →