English
There is a natural ring isomorphism between the separated quotient of a ring α and the quotient ring α/(closure of 0).
Русский
Существует естественный кольцевой изоморфизм между разделенным фактором кольца α и факторкольцом α/(closure of 0).
LaTeX
$$$$ \mathrm{sepQuotRingEquivRingQuot}(\alpha) : \mathrm{SeparationQuotient}(\alpha) \cong \alpha / \overline{(0)} $$$$
Lean4
instance topologicalRing [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
IsTopologicalRing (SeparationQuotient α)
where
toContinuousAdd := (sepQuotHomeomorphRingQuot α).isInducing.continuousAdd (sepQuotRingEquivRingQuot α)
toContinuousMul := (sepQuotHomeomorphRingQuot α).isInducing.continuousMul (sepQuotRingEquivRingQuot α)
toContinuousNeg := (sepQuotHomeomorphRingQuot α).isInducing.continuousNeg <| map_neg (sepQuotRingEquivRingQuot α)
