Theorem Bundle.mdifferentiableOn_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.mdifferentiableOn_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.mdifferentiableOn_zeroSection View on Github →