Commit 2025-12-06 21:07 b1f5e07f

feat(Geometry/Manifold): mdifferentiability of finset sums/prods (#32514) Show that a finite sum or product of mdifferentiable functions is mdifferentiable (with the expected derivative), and analogues for MDifferentiableOn, MDifferentiableWithinAt, etc.