blockDiagonal_sub — Mathlib

English

BlockDiagonal respects subtraction: blockDiagonal(M - N) = blockDiagonal(M) - blockDiagonal(N).

Русский

BlockDiagonal сохраняет вычитание: blockDiagonal(M − N) = blockDiagonal(M) − blockDiagonal(N).

LaTeX

$$$\operatorname{blockDiagonal}(M - N) = \operatorname{blockDiagonal}(M) - \operatorname{blockDiagonal}(N).$$$

Lean4

@[simp]
theorem blockDiagonal_sub [AddGroup α] (M N : o → Matrix m n α) :
    blockDiagonal (M - N) = blockDiagonal M - blockDiagonal N :=
  map_sub (blockDiagonalAddMonoidHom m n o α) M N

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