Documentation

Mathlib.Topology.Algebra.Ring.Ideal

Ideals and quotients of topological rings #

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

def Ideal.closure {R : Type u_1} [TopologicalSpace R] [Ring R] [TopologicalRing R] (I : Ideal R) :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Ideal.coe_closure {R : Type u_1} [TopologicalSpace R] [Ring R] [TopologicalRing R] (I : Ideal R) :
    ↑(Ideal.closure I) = closure I
    Equations