Commit 2025-07-03 22:04 8e1a2818

View on Github →

chore(Geometry/Manifold/VectorBundle/Basic): make some arguments implicit (#26677) All of these are in iff lemmas, which are almost always used for rewriting, and occur on both sides of the equation. Part of the path towards geodesics and the Levi-Civita connection. Co-authored by: @PatrickMassot

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

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

modified theorem Bundle.contMDiffAt_section

modified theorem Bundle.contMDiffAt_totalSpace

modified theorem Bundle.contMDiffWithinAt_section

modified theorem Bundle.contMDiffWithinAt_totalSpace

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

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