Mathlib Changelog
v4
Changelog
About
Github
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