mathlib
fa8b7ba2 - chore(topology/*): use dot notation for `is_open.prod` and `is_closed.prod` (#4510)

Commit
5 years ago
chore(topology/*): use dot notation for `is_open.prod` and `is_closed.prod` (#4510)
Author
Parents
Loading