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