Theorem HasMFDerivWithinAt.mfderivWithin_eq_zero

Modification history

2024-12-14 13:50
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: drop an assumption in `mfderivWithin_const` (#19936) …
Added HasMFDerivWithinAt.mfderivWithin_eq_zeroView on Github →