Commit 2026-09-08 09:08 07a71ad2

feat: add mvfderivWithin_eq_fderivWithin and mvfderiv_eq_fderiv (#42443) This provides missing basic API for mvfderiv, fully analogous to their mfderiv analogues. Unlike the mfderiv versions, the new lemmas are type-correct: they don't implicitly use the identification of the tangent space at a vector space with the vector space. For this reason, we derive the mfderiv lemmas from their mvfderiv versions --- and move them to MFDeriv/NormedSpace.lean to do so. We also un-simp the mfderiv lemmas, given that they introduce (mild) defeq abuse. Nothing in mathlib relied on this.