instIsTopologicalRing — Mathlib

English

If R is a topological ring, then MvPowerSeries σ R is a topological ring.

Русский

Если R — топологическое кольцо, то MvPowerSeries σ R — топологическое кольцо.

LaTeX

$$IsTopologicalRing (MvPowerSeries σ R)$$

Lean4

/-- The ring topology on `MvPowerSeries` of a topological ring -/
@[scoped instance]
theorem instIsTopologicalRing [Ring R] [IsTopologicalRing R] : IsTopologicalRing (MvPowerSeries σ R) :=
  { instIsTopologicalSemiring σ R with
    continuous_neg := continuous_pi fun d ↦ Continuous.comp continuous_neg (continuous_coeff R d) }

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