Theorem contMDiffWithinAt_hom_bundle

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 contMDiffWithinAt_hom_bundleView on Github →