Theorem mvfderiv_zero

Modification history

2026-10-17 16:48
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore: reorder mvfderiv lemmas (#43987) …
Modified mvfderiv_zeroView on Github →
2026-09-22 20:19
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore: golf mvfderiv(Within)_zero (#43986) …
Modified mvfderiv_zeroView on Github →
2026-05-20 07:15
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: add and use custom (d)elaborators for `mvfderiv`, add basic API lemmas (#39554) …
Modified mvfderiv_zeroView on Github →
2026-05-18 11:50
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore: rename extDerivFun to mvfderiv (#39485) …
Added mvfderiv_zeroView on Github →