Commit 2026-03-05 11:23 0bc810bd

View on Github →

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

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

modified theorem Bundle.mdifferentiableAt_zeroSection

modified theorem Bundle.mdifferentiableOn_zeroSection

modified theorem Bundle.mdifferentiable_zeroSection

modified theorem MDifferentiableAt.smul_section

modified theorem MDifferentiableOn.smul_section

modified theorem mdifferentiable_neg_section

modified theorem mdifferentiable_smul_section