Commit 2026-03-02 19:44 20ac8f0e

View on Github →

chore(SmoothSection): golf using custom elaborators (#35728)

Estimated changes

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

modified theorem ContMDiff.add_section

modified theorem ContMDiff.const_smul_section

modified theorem ContMDiff.neg_section

modified theorem ContMDiff.smul_section

modified theorem ContMDiff.sub_section

modified theorem ContMDiff.sum_section

modified theorem ContMDiffAt.add_section

modified theorem ContMDiffAt.const_smul_section

modified theorem ContMDiffAt.neg_section

modified theorem ContMDiffAt.smul_section

modified theorem ContMDiffAt.sub_section

modified theorem ContMDiffAt.sum_section

modified theorem ContMDiffOn.add_section

modified theorem ContMDiffOn.const_smul_section

modified theorem ContMDiffOn.neg_section

modified theorem ContMDiffOn.smul_section

modified theorem ContMDiffOn.smul_section_of_tsupport

modified theorem ContMDiffOn.sub_section

modified theorem ContMDiffSection.coeFn_mk

modified theorem ContMDiffWithinAt.add_section

modified theorem ContMDiffWithinAt.smul_section

modified theorem ContMDiffWithinAt.sub_section