English
The entries of the image of r in the algebra of CStarMatrix n×n A are diagonal with algebraMap_R,A r on the diagonal and zero elsewhere.
Русский
Коэффициенты изображения r в алгебре CStarMatrix_{n×n}(A) по диагонали равны algebraMap_R,A r, а вне диагонали—нулевые.
LaTeX
$$$(\mathrm{algebraMap}\ R\ (C^*\text{-Matrix}_{n\times n} A)\ r)_{ij} = \begin{cases} \mathrm{algebraMap}\ R\ A\ r & i=j \\ 0 & i\neq j \end{cases}$$$
Lean4
theorem algebraMap_apply [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring A] [Algebra R A] {r : R} {i j : n} :
(algebraMap R (CStarMatrix n n A) r) i j = if i = j then algebraMap R A r else 0 :=
rfl