Commit 2025-07-07 15:58 edc0f5cf
View on Github →feat(Mathlib/Order/Filter/Basic): add EventuallyEq.mul_left
and ...right
(#26852)
Add two basic lemmas which are particularly convenient when used with dot notation.
feat(Mathlib/Order/Filter/Basic): add EventuallyEq.mul_left
and ...right
(#26852)
Add two basic lemmas which are particularly convenient when used with dot notation.