Theorem MDifferentiableOn.smul_section_of_tsupport

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 MDifferentiableOn.smul_section_of_tsupportView on Github →