Theorem MDifferentiableOn.smul_section

Modification history

2026-03-05 11:23
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
chore(Geometry/Manifold/VectorBundle/MDifferentiable): golf using cus… (#36011) …
Modified MDifferentiableOn.smul_sectionView on Github →
2025-09-27 10:51
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
feat: finite sum, difference, scalar product of differentiable sections is differentiable (#26871) …
Added MDifferentiableOn.smul_sectionView on Github →