topologicalRing — Mathlib

English

The matrix space M_{n×n}(R) forms a topological ring when R is a ring with a compatible topology.

Русский

Матрицы M_{n×n}(R) образуют топологическое кольцо при условии совместимостиTopology R и кольца.

LaTeX

$$$\\operatorname{IsTopologicalRing}(\\mathrm{M}_{n\\times n}(R)).$$$

Lean4

instance topologicalRing [Fintype n] [NonUnitalNonAssocRing R] [IsTopologicalRing R] : IsTopologicalRing (Matrix n n R)
    where

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