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.

Estimated changes