Commit 2026-05-16 15:19 3ed173e4
View on Github →feat: mfderivWithin_{add,neg,sub} (#39451)
Add some lemmas for HasMFDerivWithinAt and mfderivWithin at whose corresponding versions
without a set already existed.
Part of #36036, i.e. from the path towards the Levi-Civita connection and fixing
defeq abuses related to tangent space and scalar multiplication in mathlib.