English
The blockDiagonal' construction defines an additive monoid homomorphism from families of blocks to the global block-diagonal matrix.
Русский
Конструкция blockDiagonal' образует гомоморфизм аддитивных моноидов от совокупности блоков к блочно-диагональной матрице.
LaTeX
$$$ \\text{blockDiagonal' AddMonoidHom} : (\\forall i, Matrix (m' i)(n' i) \\alpha) \\to+ M(\\Sigma i, m' i) (\\Sigma i, n' i) \\alpha $; in particular, preserves 0 and +: blockDiagonal'(0)=0 and blockDiagonal'(M+N)=blockDiagonal'M+blockDiagonal'N.$$
Lean4
/-- `Matrix.blockDiagonal'` as an `AddMonoidHom`. -/
@[simps]
def blockDiagonal'AddMonoidHom [AddZeroClass α] : (∀ i, Matrix (m' i) (n' i) α) →+ Matrix (Σ i, m' i) (Σ i, n' i) α
where
toFun := blockDiagonal'
map_zero' := blockDiagonal'_zero
map_add' := blockDiagonal'_add
