fromBlocks_submatrix_sum_swap_sum_swap

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

Похожие утверждения