instIsTopologicalRing — Mathlib

English

If each R_i is a topological ring, then the product ∀ i, R_i is a topological ring.

Русский

Если каждый R_i — топологическое кольцо, то произведение ∀ i, R_i — топологическое кольцо.

LaTeX

$$IsTopologicalRing (∀ i, R i)$$

Lean4

instance instIsTopologicalRing {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)]
    [∀ i, NonUnitalNonAssocRing (R i)] [∀ i, IsTopologicalRing (R i)] : IsTopologicalRing (∀ i, R i) :=
  ⟨⟩

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