Commit 2026-05-18 11:50 a6895680

chore: rename extDerivFun to mvfderiv (#39485) and generalise to functions taking value in any normed space. (This could be generalised to functions into additive torsors over abelian Lie groups: as we don't have this definition yet and don't need it in our applications, we leave this for the future.) The new name better reflects that this object is vector-valued. Future PRs will add further API lemmas (such as, about subtraction and negation), custom elaborators and delaborators and a version within a set. Part of #36036, i.e. from the path towards the Levi-Civita connection and Riemanian curvature. Related to fixing defeq abuses related to tangent space and scalar multiplication in mathlib.