English
Let n be finite and A be an algebra over a commutative semiring R. Then the set of n-by-n matrices with entries in A, equipped with the usual matrix operations, carries a natural structure of an R-algebra; equivalently, CStarMatrix(n,n,A) forms an Algebra over R.
Русский
Пусть n конечен, A — алгебра над коммутативной полумылью R. Тогда множество матриц размером n×n с элементами из A, оснащённое обычной операцией умножения матриц и суммирования, естественным образом образует R-алгебру; то есть CStarMatrix(n,n,A) является алгеброй над R.
LaTeX
$$$C^*\text{-Matrix}_{n\times n}(A)$ имеет структуру $R$-алгебры.$$
Lean4
instance instAlgebra [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring A] [Algebra R A] :
Algebra R (CStarMatrix n n A) :=
inferInstanceAs <| Algebra R (Matrix n n A)
