instNonUnitalNormedCommRing — Mathlib

English

If α is compact and R is a normed commutative ring without a multiplicative unit, then C(α, R) forms a NonUnitalNormedCommRing under pointwise operations, i.e., a commutative normed ring without 1.

Русский

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

LaTeX

$$$C(\alpha, R)$ является ненулевым нормированным коммутативным кольцом без единицы с операциями $(f+g)(x)=f(x)+g(x)$ и $(fg)(x)=f(x)g(x)$, и нормой $\|f\|=\sup_{x\in\alpha}\|f(x)\|$.$$

Lean4

instance [NonUnitalNormedCommRing R] : NonUnitalNormedCommRing C(α, R)
    where
  __ : NonUnitalNormedRing C(α, R) := inferInstance
  __ : NonUnitalCommRing C(α, R) := inferInstance

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