blockDiagAddMonoidHom — Mathlib

English

BlockDiag defines an additive monoid hom from matrices to functions o → matrices.

Русский

BlockDiag задаёт аддитивную гомоморфию от матриц к функциям по индексу блока.

LaTeX

$$$ \text{blockDiagAddMonoidHom} : \text{Matrix} (m×o) (n×o) α \to_+ o \to \text{Matrix} m n α \quad \text{is defined by }$$

Lean4

/-- `Matrix.blockDiag` as an `AddMonoidHom`. -/
@[simps]
def blockDiagAddMonoidHom [AddZeroClass α] : Matrix (m × o) (n × o) α →+ o → Matrix m n α
    where
  toFun := blockDiag
  map_zero' := blockDiag_zero
  map_add' := blockDiag_add

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