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