English
BlockDiagonal' preserves addition: 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'_add [AddZeroClass α] (M N : ∀ i, Matrix (m' i) (n' i) α) :
blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N :=
by
ext
simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]
split_ifs <;> simp