English
Let A, B, C, D be blocks and f pick out indices via p→l⊕m. Then the submatrix with Sum.swap on the left equals the submatrix of the swapped blocks: (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f.
Русский
Пусть A, B, C, D — блоки, а f выбирает индексы так, что f: p → l ⊕ m. Тогда подматрица со.swap слева равна подматрице переставленных блоков: (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f.
LaTeX
$$$ (\\text{fromBlocks } A \\ B \\ C \\ D).\\text{submatrix Sum.swap } f = (\\text{fromBlocks } C \\ D \\ A \\ B).\\text{submatrix } id f $$$
Lean4
@[simp]
theorem fromBlocks_submatrix_sum_swap_left (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α)
(f : p → l ⊕ m) : (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f :=
by
ext i j
cases i <;> dsimp <;> cases f j <;> rfl
