English
For blocks A,B,C,D, the double Sum.swap submatrix of the block matrix equals the reversed block matrix: (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A.
Русский
Для блоков A,B,C,D двойная подматрица Sum.swap (с заменой) блока равна обратной блочной матрице: (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A.
LaTeX
$$$ (\\text{fromBlocks } A \\ B \\ C \\ D).\\text{submatrix Sum.swap Sum.swap} = \\text{fromBlocks } D \\ C \\ B \\ A $$$
Lean4
theorem fromBlocks_submatrix_sum_swap_sum_swap {l m n o α : Type*} (A : Matrix n l α) (B : Matrix n m α)
(C : Matrix o l α) (D : Matrix o m α) : (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A := by
simp