Theorems · Definition · ring theory

Ideal.closure

{R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsTopologicalRing R] → Ideal R → Ideal R

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

Defined in

Mathlib.Topology.Algebra.Ring.Ideal

Cited by

8 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceRingIsTopologicalRing