Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-31 16:05 78f647f8

View on Github →

chore(order/filter, topology/algebra): golf (#18097)

Estimated changes