mathlib
7617942c - feat(order/filter/basic): add `filter.eventually_{eq,le}.prod_map` (#13103)

Commit

3 years ago

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

Author

urkud

urkud

Parents

Loading