instIsTopologicalRing — Mathlib

English

If R is a topological ring and S ≤ R is a subring, then S, endowed with the subspace topology, is a topological ring.

Русский

Если R — топологическое кольцо, и S ≤ R — подкольцо, то S с подпространственной топологией является топологическим кольцом.

LaTeX

$$IsTopologicalRing S$$

Lean4

instance instIsTopologicalRing (S : Subring R) : IsTopologicalRing S :=
  { S.toSubmonoid.continuousMul, inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup) with }

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