Theorem MDifferentiableAt.finsum_section_of_locallyFinite

Modification history

2025-09-27 12:35
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
feat: `finsum` and locally finite sums of differentiable sections are differentiable (#29686) …
Added MDifferentiableAt.finsum_section_of_locallyFiniteView on Github →