Commit 2025-07-10 17:00 1baac3c7

feat: contMDiff_section_of_tsupport (#26671) A scalar product f • s of a C^k function f : M → ℝ with a section s is C^k once s is C^k on an open subset containing tsupport s. In particular, this applies to proving the smoothness of a section paired with a smooth bump function. This is more general than contMDiff_of_tsupportsince the co-domain is the total space of a vector bundle, which does not have aZero`. Part of the path towards the geodesics and the Levi-Civita connection.