Theorem ContMDiffOn.smul_section_of_tsupport

Modification history

2026-03-02 19:44
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
chore(SmoothSection): golf using custom elaborators (#35728)
Modified ContMDiffOn.smul_section_of_tsupportView on Github →
2025-07-22 18:37
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
feat: sum of a locally finite collection of C^n sections is C^n (#27349) …
Modified ContMDiffOn.smul_section_of_tsupportView on Github →
2025-07-10 17:00
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
feat: `contMDiff_section_of_tsupport` (#26671) …
Added ContMDiffOn.smul_section_of_tsupportView on Github →