scalar — Mathlib

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 α

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