Yeah, this is a continuing point of confusion. Partial derivatives are really more of a teaching tool. The real truth is that the derivative of a map $$E \to F$$ is a map $$E \to Hom(E, F)$$ so this is how we do things in Mathlib (via fderiv). Possibly some day someone will make a sufficiently compelling case to define partial derivatives (relative to bases) but that hasn't happened yet.
EDIT:
Annoyingly (or appropriately) I've just discovered my fix using fderivstill contained an error (fix proposed in https://github.com/trishullab/PutnamBench/pull/210). Partly this is because it's so hard not to make a mistake when formalising statements only, but I have to confess if Mathlib contained an abbrev for partial derivatives of functions (Fin n → 𝕜) → (Fin m → 𝕜) then I don't think this would have happened.
Yeah, this is a continuing point of confusion. Partial derivatives are really more of a teaching tool. The real truth is that the derivative of a map $$E \to F$$ is a map $$E \to Hom(E, F)$$ so this is how we do things in Mathlib (via
fderiv). Possibly some day someone will make a sufficiently compelling case to define partial derivatives (relative to bases) but that hasn't happened yet.EDIT: Annoyingly (or appropriately) I've just discovered my fix using
fderivstill contained an error (fix proposed in https://github.com/trishullab/PutnamBench/pull/210). Partly this is because it's so hard not to make a mistake when formalising statements only, but I have to confess if Mathlib contained anabbrevfor partial derivatives of functions(Fin n → 𝕜) → (Fin m → 𝕜)then I don't think this would have happened.