mathlib
b1aafb20 - fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647)

Commit
4 years ago
fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647) Everything had type max{u v} before.
Author
Parents
Loading