Commit 2025-07-07 13:19 67db308b

View on Github →

feat: finite sum, difference, scalar product of C^k sections is C^k (#26674) And use this to golf the proofs in SmoothSection.lean. A future PR will add the analogous results for differentiability of sections. Part of the path towards the geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem ContMDiff.add_section

added theorem ContMDiff.const_smul_section

added theorem ContMDiff.neg_section

added theorem ContMDiff.smul_section

added theorem ContMDiff.sub_section

added theorem ContMDiff.sum_section

added theorem ContMDiffAt.add_section

added theorem ContMDiffAt.const_smul_section

added theorem ContMDiffAt.neg_section

added theorem ContMDiffAt.smul_section

added theorem ContMDiffAt.sub_section

added theorem ContMDiffAt.sum_section

added theorem ContMDiffOn.add_section

added theorem ContMDiffOn.const_smul_section

added theorem ContMDiffOn.neg_section

added theorem ContMDiffOn.smul_section

added theorem ContMDiffOn.sub_section

added theorem ContMDiffOn.sum_section

added theorem ContMDiffWithinAt.add_section

added theorem ContMDiffWithinAt.const_smul_section

added theorem ContMDiffWithinAt.neg_section

added theorem ContMDiffWithinAt.smul_section

added theorem ContMDiffWithinAt.sub_section

added theorem ContMDiffWithinAt.sum_section