instIsTopologicalRing — Mathlib

English

PowerSeries(R) is a topological ring provided R is a topological ring.

Русский

PowerSeries(R) является топологическим кольцом, если R — топологическое кольцо.

LaTeX

$$$ \\text{IsTopologicalRing}(\\PowerSeries(R)) $$$

Lean4

/-- The ring topology on `PowerSeries` of a topological ring -/
@[scoped instance]
theorem instIsTopologicalRing [Ring R] [IsTopologicalRing R] : IsTopologicalRing (PowerSeries R) :=
  MvPowerSeries.WithPiTopology.instIsTopologicalRing Unit R

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