Theorem Filter.EventuallyEq.mfderiv_eq

Modification history

2026-08-20 12:42
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore: fix defeq abuse in the definition of MFDeriv (#42193) …
Modified Filter.EventuallyEq.mfderiv_eqView on Github →
2026-07-17 10:49
Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803) …
Modified Filter.EventuallyEq.mfderiv_eqView on Github →
2023-06-26 19:57
Mathlib/Geometry/Manifold/MFDeriv.lean
feat: port Geometry.Manifold.Mfderiv (#5454)
Added Filter.EventuallyEq.mfderiv_eqView on Github →