Theorem extDerivFun_zero

Modification history

2026-05-18 11:50
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore: rename extDerivFun to mvfderiv (#39485) …
Deleted extDerivFun_zeroView on Github →
2026-03-12 19:24
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: covariant derivatives on vector bundles (#36279) …
Added extDerivFun_zeroView on Github →