Theorem mdifferentiableOn_congr

Modification history

2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified mdifferentiableOn_congrView on Github →
2025-07-04 16:11
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
feat: missing congruence lemmas for mdifferentiability (#26709) …
Added mdifferentiableOn_congrView on Github →