Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-02 22:23 7617942c

View on Github →

feat(order/filter/basic): add filter.eventually_{eq,le}.prod_map (#13103)

Estimated changes