Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_ordered_comm_group_with_zero.nhds_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) …
Deleted linear_ordered_comm_group_with_zero.nhds_zeroView on Github →
2022-09-19 07:18
src/topology/algebra/with_zero_topology.lean
refactor(topology/algebra/with_zero_topology): review API, golf (#16359) …
Added linear_ordered_comm_group_with_zero.nhds_zeroView on Github →