Theorem HasMFDerivAt.congr_of_eventuallyEq_abuse

Modification history

2026-08-20 12:42
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore: fix defeq abuse in the definition of MFDeriv (#42193) …
Added HasMFDerivAt.congr_of_eventuallyEq_abuseView on Github →