English
There is a ring equivalence between the separated quotient of a topological ring α and the quotient ring α/(⊥ : Ideal α).closure.
Русский
Существуют:ring-эквивалентности между отделённой фактор-группой кольца α и фактор-группой α/(⊥). closure.
LaTeX
$$$\mathrm{sepQuotRingEquivRingQuot}(\alpha): \mathrm{SeparationQuotient}(\alpha) \cong+* \alpha / (\bot : \mathrm{Ideal}\ \alpha).\mathrm{closure}$$$
Lean4
/-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
continuous, get an equivalence between the separated quotient of `α` and the quotient ring
corresponding to the closure of zero. -/
def sepQuotRingEquivRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
SeparationQuotient α ≃+* α ⧸ (⊥ : Ideal α).closure :=
(sepQuotHomeomorphRingQuot _).ringEquiv
