algebraMap_eq_diagonal — Mathlib

English

The algebra map from R into M_n(α) coincides with the diagonal embedding of the function space R → α into diagonal matrices.

Русский

Отображение R в M_n(α) совпадает с диагональным вложением функции R → α в диагональные матрицы.

LaTeX

$$algebraMap R (Matrix n n α) = diagonal (algebraMap R (n → α))$$

Lean4

theorem algebraMap_eq_diagonal (r : R) : algebraMap R (Matrix n n α) r = diagonal (algebraMap R (n → α) r) :=
  rfl

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