Theorem MDifferentiableWithinAt.sum

Modification history

2025-12-06 21:07
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat(Geometry/Manifold): mdifferentiability of finset sums/prods (#32514) …
Added MDifferentiableWithinAt.sumView on Github →