Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_zero_topology.singleton_mem_nhds_of_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.singleton_mem_nhds_of_unitsView on Github →