with_zero_topology): move to a new NS, used `localized` (#18560)

Commit

2 years ago

chore(topology/algebra/with_zero_topology): move to a new NS, used `localized` (#18560) This way we can naturally use `scoped instance` in Lean 4.

Author

urkud

Parents