diagonalRingHom — Mathlib

English

There is a natural 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

$$$\\text{diagonalRingHom}: α \\to^+* M_n(α)\\; (a \\mapsto \\operatorname{diag}(a))$$$

Lean4

/-- `Matrix.diagonal` as a `RingHom`. -/
@[simps]
def diagonalRingHom [Fintype n] [DecidableEq n] : (n → α) →+* Matrix n n α :=
  { diagonalAddMonoidHom n α with
    toFun := diagonal
    map_one' := diagonal_one
    map_mul' := fun _ _ => (diagonal_mul_diagonal' _ _).symm }

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