Theorem ContMDiffAt.const_smul_section

Modification history

2026-03-02 19:44
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
chore(SmoothSection): golf using custom elaborators (#35728)
Modified ContMDiffAt.const_smul_sectionView on Github →
2025-07-07 13:19
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
feat: finite sum, difference, scalar product of `C^k` sections is `C^k` (#26674) …
Added ContMDiffAt.const_smul_sectionView on Github →