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.
fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647) Everything had type max{u v} before.