Theorem ContMDiff.clm_bundle_apply

Modification history

2025-06-19 19:33
Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
feat: applying a smooth hom bundle section to a smooth section gives a smooth section (#26112)
Added ContMDiff.clm_bundle_applyView on Github →