Theorem mvfderivWithin_smul

Modification history

2026-05-31 10:14
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: add `mvfderivWithin` with (d)elaborators and basic API (#39513) …
Added mvfderivWithin_smulView on Github →