Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-08 09:51 3e0c4d76

View on Github →

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.

Estimated changes

Modified src/topology/algebra/valued_field.lean

Modified src/topology/algebra/with_zero_topology.lean

deleted theorem linear_ordered_comm_group_with_zero.Iio_mem_nhds

deleted theorem linear_ordered_comm_group_with_zero.Iio_mem_nhds_zero

deleted theorem linear_ordered_comm_group_with_zero.has_basis_nhds_of_ne_zero

deleted theorem linear_ordered_comm_group_with_zero.has_basis_nhds_units

deleted theorem linear_ordered_comm_group_with_zero.has_basis_nhds_zero

deleted theorem linear_ordered_comm_group_with_zero.is_closed_iff

deleted theorem linear_ordered_comm_group_with_zero.is_open_Iio

deleted theorem linear_ordered_comm_group_with_zero.is_open_iff

deleted theorem linear_ordered_comm_group_with_zero.nhds_coe_units

deleted theorem linear_ordered_comm_group_with_zero.nhds_eq_update

deleted theorem linear_ordered_comm_group_with_zero.nhds_of_ne_zero

deleted theorem linear_ordered_comm_group_with_zero.nhds_zero

deleted theorem linear_ordered_comm_group_with_zero.nhds_zero_of_units

deleted theorem linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_ne_zero

deleted theorem linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_units

deleted theorem linear_ordered_comm_group_with_zero.tendsto_of_ne_zero

deleted theorem linear_ordered_comm_group_with_zero.tendsto_units

deleted theorem linear_ordered_comm_group_with_zero.tendsto_zero

added theorem with_zero_topology.Iio_mem_nhds

added theorem with_zero_topology.Iio_mem_nhds_zero

added theorem with_zero_topology.has_basis_nhds_of_ne_zero

added theorem with_zero_topology.has_basis_nhds_units

added theorem with_zero_topology.has_basis_nhds_zero

added theorem with_zero_topology.is_closed_iff

added theorem with_zero_topology.is_open_Iio

added theorem with_zero_topology.is_open_iff

added theorem with_zero_topology.nhds_coe_units

added theorem with_zero_topology.nhds_eq_update

added theorem with_zero_topology.nhds_of_ne_zero

added theorem with_zero_topology.nhds_zero

added theorem with_zero_topology.nhds_zero_of_units

added theorem with_zero_topology.singleton_mem_nhds_of_ne_zero

added theorem with_zero_topology.singleton_mem_nhds_of_units

added theorem with_zero_topology.t3_space

added theorem with_zero_topology.tendsto_of_ne_zero

added theorem with_zero_topology.tendsto_units

added theorem with_zero_topology.tendsto_zero