Commit 2025-07-04 16:11 26ee3425

View on Github →

feat: missing congruence lemmas for mdifferentiability (#26709) Each of these lemmas has a ContMDiff analogue, this is how this PR was made. From the path towards geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem Filter.EventuallyEq.mdifferentiableAt_iff

added theorem Filter.EventuallyEq.mdifferentiablefWithinAt_iff

added theorem MDifferentiableOn.congr

added theorem MDifferentiableWithinAt.congr_of_mem

added theorem mdifferentiableOn_congr

added theorem mdifferentiableWithinAt_congr

added theorem mdifferentiableWithinAt_congr_of_mem