English
There is a canonical ring homomorphism from α to the matrix ring M_n(α) sending a to the diagonal matrix with a on the diagonal.
Русский
Существует каноническое вложение из α в M_n(α), отправляющее скаляр a в диагональную матрицу diag(a).
LaTeX
$$def scalar (n) [DecidableEq n] [Fintype n] : α →+* Matrix n n α$$
Lean4
/-- The ring homomorphism `α →+* Matrix n n α`
sending `a` to the diagonal matrix with `a` on the diagonal.
-/
def scalar (n : Type u) [DecidableEq n] [Fintype n] : α →+* Matrix n n α :=
(diagonalRingHom n α).comp <| Pi.constRingHom n α