Commit 2025-09-27 10:51 12130d8f

View on Github →

feat: finite sum, difference, scalar product of differentiable sections is differentiable (#26871) This mirrors the additions of #26674 to mdifferentiable sections. Part of the path towards geodesics and the Levi-Civita connection.

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

added theorem MDifferentiable.sum_section

added theorem MDifferentiableAt.smul_const_section

added theorem MDifferentiableAt.smul_section

added theorem MDifferentiableAt.sum_section

added theorem MDifferentiableOn.smul_const_section

added theorem MDifferentiableOn.smul_section

added theorem MDifferentiableOn.sum_section

added theorem MDifferentiableWithinAt.smul_section

added theorem MDifferentiableWithinAt.sum_section

added theorem mDifferentiableOn_sub_section

added theorem mdifferentiableAt_add_section

added theorem mdifferentiableAt_neg_section

added theorem mdifferentiableAt_sub_section

added theorem mdifferentiableOn_add_section

added theorem mdifferentiableOn_neg_section

added theorem mdifferentiableWithinAt_add_section

added theorem mdifferentiableWithinAt_neg_section

added theorem mdifferentiableWithinAt_smul_const_section

added theorem mdifferentiableWithinAt_sub_section

added theorem mdifferentiable_add_section

added theorem mdifferentiable_neg_section

added theorem mdifferentiable_smul_const_section

added theorem mdifferentiable_smul_section

added theorem mdifferentiable_sub_section