algebraMap_apply — Mathlib

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

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