blockDiagonal'_sub — Mathlib

English

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

Русский

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

LaTeX

$$$ \\mathrm{blockDiagonal}'(M - N) = \\mathrm{blockDiagonal}' M - \\mathrm{blockDiagonal}' N $$$

Lean4

@[simp]
theorem blockDiagonal'_sub [AddGroup α] (M N : ∀ i, Matrix (m' i) (n' i) α) :
    blockDiagonal' (M - N) = blockDiagonal' M - blockDiagonal' N :=
  map_sub (blockDiagonal'AddMonoidHom m' n' α) M N

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