instIsTopologicalRing — Mathlib

English

The subalgebra s of a topological ring A inherits a natural topological ring structure from A; i.e., s is a topological ring.

Русский

Подалгебра s над топологическим кольцом A наследует естественную топологическую структуру кольца; то есть s является топологическим кольцом.

LaTeX

$$$IsTopologicalRing(s)$$$

Lean4

instance instIsTopologicalRing (s : NonUnitalSubalgebra R A) : IsTopologicalRing s :=
  s.toNonUnitalSubring.instIsTopologicalRing

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