toBlocks_fromBlocks₁₁ — Mathlib

English

Extracting the top-left block from fromBlocks returns A.

Русский

Извлечение верхне-левого блока из fromBlocks возвращает A.

LaTeX

$$toBlocks_fromBlocks₁₁ (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) : (fromBlocks A B C D).toBlocks₁₁ = A$$

Lean4

@[simp]
theorem toBlocks_fromBlocks₁₁ (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
    (fromBlocks A B C D).toBlocks₁₁ = A :=
  rfl

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