Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_zero_topology.has_basis_nhds_of_ne_zero

Modification history

2023-03-08 09:51

src/topology/algebra/with_zero_topology.lean

chore(topology/algebra/with_zero_topology): move to a new NS, used `localized` (#18560) …

Added with_zero_topology.has_basis_nhds_of_ne_zero View on Github →