mathlib
f2ce6086 - chore(*): rename locale `topological_space` to `topology` (#18293)

Commit

2 years ago

chore(*): rename locale `topological_space` to `topology` (#18293)

Author

urkud

urkud

Parents

Loading