Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_zero_topology.has_basis_nhds_units

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_unitsView on Github →