Theorem Bundle.mdifferentiableWithinAt_zeroSection

Modification history

2025-07-07 20:08
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
feat(VectorBundle/MDifferentiable): add some basic API (#26865) …
Added Bundle.mdifferentiableWithinAt_zeroSectionView on Github →