Commit 2025-06-18 14:59 5b77ef3c

View on Github →

feat: drop an assumption in congruence lemma for manifold derivatives (#25771)

Estimated changes

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

added theorem ContMDiffAt.comp_contMDiffWithinAt_of_eq

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

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

modified theorem Filter.EventuallyEq.mfderivWithin_eq

added theorem Filter.EventuallyEq.mfderivWithin_eq_of_mem

modified theorem mfderivWithin_congr

added theorem mfderivWithin_congr_of_mem

modified theorem tangentMapWithin_congr