topologicalRing_quotient — Mathlib

English

The quotient ring R/N inherits a topology making mk N a quotient map and continuous with multiplication.

Русский

Кольцо R/N наследует топологию, делающую mk N фактор-мэппингом и непрерывным по операции умножения.

LaTeX

$$$ IsTopologicalRing (HasQuotient.Quotient R N) $$$

Lean4

instance topologicalRing_quotient : IsTopologicalRing (R ⧸ N)
    where
  __ := QuotientAddGroup.instIsTopologicalAddGroup _
  continuous_mul := (QuotientRing.isQuotientMap_coe_coe N).continuous_iff.2 <| continuous_quot_mk.comp continuous_mul

Похожие утверждения