Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-02 00:11 9a59dcb7

View on Github →

chore(topology/algebra/ring): split into 2 files (#18532)

Estimated changes

Modified src/analysis/normed/group/infinite_sum.lean

Modified src/analysis/normed_space/units.lean

Modified src/topology/algebra/field.lean

Modified src/topology/algebra/infinite_sum/real.lean

Modified src/topology/algebra/infinite_sum/ring.lean

Modified src/topology/algebra/localization.lean

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

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

Modified src/topology/algebra/open_subgroup.lean

Modified src/topology/algebra/order/field.lean

Renamed src/topology/algebra/ring.lean to src/topology/algebra/ring/basic.lean

deleted def ideal.closure

deleted theorem ideal.closure_eq_of_is_closed

deleted theorem ideal.coe_closure

deleted theorem quotient_ring.is_open_map_coe

deleted theorem quotient_ring.quotient_map_coe_coe

Created src/topology/algebra/ring/ideal.lean

added theorem ideal.closure_eq_of_is_closed

added theorem ideal.coe_closure

added theorem quotient_ring.is_open_map_coe

added theorem quotient_ring.quotient_map_coe_coe

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/category/TopCommRing.lean

Modified src/topology/instances/matrix.lean

Modified src/topology/instances/real.lean