Theorem HasMFDerivWithinAt.congr_mfderiv

Modification history

2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified HasMFDerivWithinAt.congr_mfderivView on Github →
2023-12-17 07:58
Mathlib/Geometry/Manifold/MFDeriv.lean
feat: Add `congr_mfderiv` lemmas mirroring `congr_fderiv` (#9066) …
Added HasMFDerivWithinAt.congr_mfderivView on Github →