mathlib documentation

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} [topological_space R] [ring R] [topological_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} [topological_space R] [ring R] [topological_ring R] (I : ideal R) :
@[simp]
theorem ideal.closure_eq_of_is_closed {R : Type u_1} [topological_space R] [ring R] [topological_ring R] (I : ideal R) [hI : is_closed I] :
@[protected, instance]