fromBlocks_transpose — Mathlib

English

For the block matrix fromBlocks A B C D, the transpose equals the block matrix with transposed blocks in swapped order: (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ.

Русский

Для блочной матрицы fromBlocks A B C D транспонирование дают как блочную матрицу с транспонированными блоками в порядке Aᵀ Cᵀ Bᵀ Dᵀ: (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ.

LaTeX

$$$ (\\text{fromBlocks } A \\ B \\ C \\ D)^T = \\text{fromBlocks } A^T C^T B^T D^T $$$

Lean4

theorem fromBlocks_transpose (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
    (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ := by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

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