blockDiagonalAddMonoidHom — Mathlib

English

BlockDiagonal induces an AddMonoidHom from o → Matrix m n α to Matrix (m × o) (n × o) α, with the same algebraic structure as componentwise blocks.

Русский

BlockDiagonal порождает гомоморфизм AddMonoidHom от семейства матриц к блочной диагонали с тем же алгебраическим строением по блочным компонентам.

LaTeX

$$(“blockDiagonalAddMonoidHom” is the AddMonoidHom structure with toFun = blockDiagonal, map_zero' = blockDiagonal_zero, map_add' = blockDiagonal_add).$$

Lean4

/-- `Matrix.blockDiagonal` as an `AddMonoidHom`. -/
@[simps]
def blockDiagonalAddMonoidHom [AddZeroClass α] : (o → Matrix m n α) →+ Matrix (m × o) (n × o) α
    where
  toFun := blockDiagonal
  map_zero' := blockDiagonal_zero
  map_add' := blockDiagonal_add

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