English
Sum of block matrices is the block matrix of sums: fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A+A') (B+B') (C+C') (D+D').
Русский
Сумма блочных матриц равна блочной матрице сумм: fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A+A') (B+B') (C+C') (D+D').
LaTeX
$$$ \\text{fromBlocks } A B C D + \\text{fromBlocks } A' B' C' D' = \\text{fromBlocks }(A + A') (B + B') (C + C') (D + D') $$$
Lean4
theorem fromBlocks_add [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α)
(A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α) (D' : Matrix o m α) :
fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D') := by ext i j;
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl
