instNonUnitalSeminormedCommRing — Mathlib

English

If R is a NonUnitalSeminormedCommRing, then C(α,R) is a NonUnitalSeminormedCommRing and multiplication is commutative: fg = gf.

Русский

Если R — NonUnitalSeminormedCommRing, тогда C(α,R) является NonUnitalSeminormedCommRing и умножение коммутативно: fg = gf.

LaTeX

$$$f\cdot g = g\cdot f$$$

Lean4

instance [NonUnitalSeminormedCommRing R] : NonUnitalSeminormedCommRing C(α, R)
    where
  __ : NonUnitalSeminormedRing C(α, R) := inferInstance
  __ : NonUnitalCommRing C(α, R) := inferInstance

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