blockDiag'AddMonoidHom — Mathlib

English

The blockDiag'AddMonoidHom construction preserves addition and zero, giving an additive monoid hom from matrices to block diagonals.

Русский

Конструкция blockDiag'AddMonoidHom сохраняет сложение и ноль, образуя аддитивный моноид-гомоморфизм.

LaTeX

$$$ \\text{blockDiag'AddMonoidHom} : (\\forall i, Matrix (m' i)(n' i) \\alpha) \\to+∀ i, Matrix (m' i)(n' i) \\alpha$; with the properties map_zero' and map_add' as above.$$

Lean4

/-- `Matrix.blockDiag'` as an `AddMonoidHom`. -/
@[simps]
def blockDiag'AddMonoidHom [AddZeroClass α] : Matrix (Σ i, m' i) (Σ i, n' i) α →+ ∀ i, Matrix (m' i) (n' i) α
    where
  toFun := blockDiag'
  map_zero' := blockDiag'_zero
  map_add' := blockDiag'_add

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