diagonalAddMonoidHom — Mathlib

English

The diagonal map diag: (n → α) → Matrix n n α is an additive monoid hom; it preserves zero and addition: diag(0) = 0 and diag(x + y) = diag(x) + diag(y).

Русский

Диагональное отображение diag: (n → α) → Matrix n n α является гомоморфизмом аддитивных моноидов: diag(0) = 0 и diag(x + y) = diag(x) + diag(y).

LaTeX

$$$\\text{diag}: (n \\to α) \\to+ Matrix\\ n\\ n\\ α$ satisfies diag(0)=0 and diag(x+y)=diag(x)+diag(y).$$

Lean4

/-- `Matrix.diagonal` as an `AddMonoidHom`. -/
@[simps]
def diagonalAddMonoidHom [AddZeroClass α] : (n → α) →+ Matrix n n α
    where
  toFun := diagonal
  map_zero' := diagonal_zero
  map_add' x y := (diagonal_add x y).symm

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