matrix): Add the uniform_space structure on matrices (#13534)

Commit

3 years ago

feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Author

eric-wieser

Parents

45470769

mathlib b98bd418 - feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534)

mathlib
b98bd418 - feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534)