instSeminormedCommRing — Mathlib

English

If R is a SeminormedCommRing, then C(α,R) is a SeminormedCommRing (commutative ring with a compatible seminorm).

Русский

Если R — SeminormedCommRing, тогда C(α,R) — SeminormedCommRing (коммутативное кольцо с совместной септимормой).

LaTeX

$$$C(\alpha,R) \text{ is a SeminormedCommRing}$$$

Lean4

instance [SeminormedCommRing R] : SeminormedCommRing C(α, R)
    where
  __ : SeminormedRing C(α, R) := inferInstance
  __ : CommRing C(α, R) := inferInstance

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