# mathlib3documentation

topology.algebra.ring.ideal

# Ideals and quotients of topological rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define ideal.closure to be the topological closure of an ideal in a topological ring. We also define a topological_space structure on the quotient of a topological ring by an ideal and prove that the quotient is a topological ring.

@[protected]
def ideal.closure {R : Type u_1} [ring R] (I : ideal R) :

The closure of an ideal in a topological ring as an ideal.

Equations
@[simp]
theorem ideal.coe_closure {R : Type u_1} [ring R] (I : ideal R) :
@[simp]
theorem ideal.closure_eq_of_is_closed {R : Type u_1} [ring R] (I : ideal R) [hI : is_closed I] :
@[protected, instance]
Equations
theorem quotient_ring.is_open_map_coe {R : Type u_1} [comm_ring R] (N : ideal R)  :
theorem quotient_ring.quotient_map_coe_coe {R : Type u_1} [comm_ring R] (N : ideal R)  :
quotient_map (λ (p : R × R), ( p.fst, p.snd))
@[protected, instance]
def topological_ring_quotient {R : Type u_1} [comm_ring R] (N : ideal R)  :