diagAddMonoidHom — Mathlib

English

The diagonal map is an AddMonoidHom: it preserves addition and maps zero to zero.

Русский

Диагональное отображение — гомоморфизм аддитивного моноида: сохраняет сложение и ноль.

LaTeX

$$$\\operatorname{diag}(0) = 0$, $\\operatorname{diag}(x+y) = \\operatorname{diag}(x) + \\operatorname{diag}(y)$$$

Lean4

/-- `Matrix.diag` as an `AddMonoidHom`. -/
@[simps]
def diagAddMonoidHom [AddZeroClass α] : Matrix n n α →+ n → α
    where
  toFun := diag
  map_zero' := diag_zero
  map_add' := diag_add

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