Theorem mvfderiv_zero

Modification history

2026-09-22 20:19

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

chore: golf mvfderiv(Within)_zero (#43986) …

Modified mvfderiv_zero View 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_zero View on Github →

2026-05-18 11:50

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

chore: rename extDerivFun to mvfderiv (#39485) …

Added mvfderiv_zero View on Github →