Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-11 22:32 b1aafb20

View on Github →

fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647) Everything had type max{u v} before.

Estimated changes