Commit 2025-07-03 21:54 92b730c9

View on Github →

feat: add missing API for MDifferentiable*.{add,neg} (#26702) Discovered while working towards geodesics and the Levi-Civita connection. Co-authored by: @PatrickMassot

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

added theorem HasMFDerivWithinAt.add

added theorem HasMFDerivWithinAt.neg

added theorem MDifferentiableOn.add

added theorem MDifferentiableOn.neg

added theorem MDifferentiableWithinAt.add

added theorem MDifferentiableWithinAt.neg