instNormedCommRing — Mathlib

English

If R is a NormedCommRing, then α →ᵇ R is a NormedCommRing with norm defined componentwise.

Русский

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

LaTeX

$$$[\\text{NormedCommRing }R] \\Rightarrow \\text{NormedCommRing}(\\alpha \\to^b R)$$$

Lean4

instance instNormedCommRing [NormedCommRing R] : NormedCommRing (α →ᵇ R)
    where
  __ := instSeminormedCommRing
  __ := instNormedAddCommGroup

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