Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 13:39 a33ab129

View on Github →

refactor(analysis/topology): move separation ring to quotient_topological_structures

Estimated changes

Modified analysis/topology/completion.lean

deleted theorem uniform_space.eq_mpr_heq

deleted theorem uniform_space.ring_sep_quot

deleted theorem uniform_space.ring_sep_rel

Modified analysis/topology/quotient_topological_structures.lean

deleted theorem is_open_map_mul_left

deleted theorem is_open_map_mul_right

deleted theorem quotient_ring.quotient_map

added theorem quotient_ring.quotient_map_coe_coe

added theorem uniform_space.ring_sep_quot

added theorem uniform_space.ring_sep_rel

added def uniform_space.sep_quot_equiv_ring_quot

added theorem {u}

Modified analysis/topology/topological_structures.lean

added theorem is_open_map_mul_left

added theorem is_open_map_mul_right