mathlib
e4515446 - doc(analysis/locally_convex/with_seminorms): fix hyperlink and add first countable (#17303)

Commit
3 years ago
doc(analysis/locally_convex/with_seminorms): fix hyperlink and add first countable (#17303) This fixes the hyperlink for `with_seminorms.to_locally_convex_space` and adds `with_seminorms.first_countable` to the module docstring.
Author
Parents
Loading