Theorem mvfderiv_const

Modification history

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) …

Added mvfderiv_const View on Github →