Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-02 15:13 c10e724b

View on Github →

refactor(topology/algebra/field): drop topological_space_units (#18536) See Zulip chat Also generalize TC assumptions in inv_mem_iff.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

modified theorem inv_mem_iff

Modified src/group_theory/subgroup/pointwise.lean

modified theorem inv_coe_set

Modified src/topology/algebra/constructions.lean

added theorem units.embedding_coe_mk

added theorem units.topology_eq_inf

Modified src/topology/algebra/field.lean

deleted theorem topological_division_ring.continuous_units_inv

deleted theorem topological_division_ring.units_top_group

deleted theorem topological_ring.induced_units.continuous_coe

deleted def topological_ring.topological_space_units

deleted theorem topological_ring.units_embedding

deleted theorem topological_ring.units_topology_eq

Modified src/topology/algebra/group/basic.lean

added def to_units_homeomorph

Modified src/topology/algebra/group_with_zero.lean

added theorem units.embedding_coe₀