instIsTopologicalRingProd — Mathlib

English

The product of two topological rings, with the product topology, is a topological ring.

Русский

Произведение топологических колец с использованием произведения топологий обладает структурой топологического кольца.

LaTeX

$$IsTopologicalRing (R × S)$$

Lean4

/-- The product topology on the Cartesian product of two topological rings
  makes the product into a topological ring. -/
instance [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [IsTopologicalRing R] [IsTopologicalRing S] :
    IsTopologicalRing (R × S) where

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