Theorem mvfderiv_eq_fderiv

Modification history

2026-09-16 15:44
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore: make m(v)fderiv(Within)_eq_fderiv(Within) more type-correct (#43521)
Modified mvfderiv_eq_fderivView on Github →
2026-09-08 09:08
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: add `mvfderivWithin_eq_fderivWithin` and `mvfderiv_eq_fderiv` (#42443) …
Added mvfderiv_eq_fderivView on Github →