instSeminormedCommRing — Mathlib

English

If R is a SeminormedCommRing, then the space α →ᵇ R inherits a SeminormedCommRing structure via pointwise operations.

Русский

Если R — семинормированное коммутативное кольцо, то пространство α →ᵇ R наследует структуру семинормированного коммутативного кольца по покоординатным операциям.

LaTeX

$$$\\text{If } [\\text{SeminormedCommRing }R] \\text{ then } (\\alpha \\to^b R) \\text{ is a SeminormedCommRing}.$$

Lean4

instance instSeminormedCommRing [SeminormedCommRing R] : SeminormedCommRing (α →ᵇ R)
    where
  __ := instCommRing
  __ := instNonUnitalSeminormedRing

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