Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 13:47 45aed677

View on Github →

chore(order/filter/basic): add filter.sup_prod and filter.prod_sup (#8572)

Estimated changes