instNonUnitalCommCStarAlgebraProd

English

The product of two nonunital commutative C*-algebras is a nonunital commutative C*-algebra.

Русский

Произведение двух немоноидных коммутативных C*-алгебр с отсутствующей единицей образует немоноидную коммутативную C*-алгебру.

LaTeX

$$instNonUnitalCommCStarAlgebraProd A B$$

Lean4

instance [NonUnitalCommCStarAlgebra A] [NonUnitalCommCStarAlgebra B] : NonUnitalCommCStarAlgebra (A × B) where

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