mathlib
6a09cd06 - chore(topology/uniform_space): use weaker TC assumptions (#12066)

Commit

3 years ago

chore(topology/uniform_space): use weaker TC assumptions (#12066) We don't need `[uniform_space β]` to prove `uniform_space.completion.ext`.

Author

urkud

Parents