instNormedCommRing — Mathlib

English

If α is compact and R is a NormedCommRing, then C(α, R) carries a NormedCommRing structure under pointwise operations.

Русский

Если α компактно, а R является нормированным коммутативным кольцом, то C(α, R) образует нормированное коммутативное кольцо по точечным операциям.

LaTeX

$$$C(\alpha, R)$ is a NormedCommRing with pointwise operations and the norm $\|f\|=\sup_{x\in\alpha}\|f(x)\|$.$$

Lean4

instance [NormedCommRing R] : NormedCommRing C(α, R)
    where
  __ : NormedRing C(α, R) := inferInstance
  __ : CommRing C(α, R) := inferInstance

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