Commit 2021-10-06 10:12 facc1d2d

View on Github →

feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537) This is a modernized version of code from the perfectoid spaces project.

Estimated changes

Modified src/algebra/order/with_zero.lean

added theorem inv_mul_lt_of_lt_mul₀

Created src/topology/algebra/with_zero_topology.lean

added theorem linear_ordered_comm_group_with_zero.directed_lt

added theorem linear_ordered_comm_group_with_zero.has_basis_nhds_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.has_basis_nhds_units

added theorem linear_ordered_comm_group_with_zero.has_basis_nhds_zero

added theorem linear_ordered_comm_group_with_zero.nhds_coe_units

added def linear_ordered_comm_group_with_zero.nhds_fun

added theorem linear_ordered_comm_group_with_zero.nhds_fun_ok

added theorem linear_ordered_comm_group_with_zero.nhds_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.nhds_zero_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.nhds_zero_of_units

added theorem linear_ordered_comm_group_with_zero.pure_le_nhds_fun

added theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_units

added theorem linear_ordered_comm_group_with_zero.tendsto_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.tendsto_units

added theorem linear_ordered_comm_group_with_zero.tendsto_zero

Modified src/topology/basic.lean

added theorem is_closed.compl_mem_nhds