isTopologicalRing — Mathlib

English

Under ring-like assumptions, the restricted product is a topological ring.

Русский

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

LaTeX

$$$\\mathrm{IsTopologicalRing}\\left(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{B_i\\}; \\mathrm{cofinite})\\right)$$$

Lean4

instance isTopologicalRing [Π i, Ring (R i)] [∀ i, SubringClass (S i) (R i)] [∀ i, IsTopologicalRing (R i)] :
    IsTopologicalRing (Πʳ i, [R i, B i]) where

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