Theorem Bundle.mdifferentiableAt_zeroSection

Modification history

2026-03-05 11:23

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

chore(Geometry/Manifold/VectorBundle/MDifferentiable): golf using cus… (#36011) …

Modified Bundle.mdifferentiableAt_zeroSection View on Github →

2025-07-07 20:08

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

feat(VectorBundle/MDifferentiable): add some basic API (#26865) …

Added Bundle.mdifferentiableAt_zeroSection View on Github →