toBlocks_fromBlocks₁₂ — Mathlib

English

Extracting the bottom-right block from fromBlocks gives D.

Русский

Извлечение нижнего правого блока из fromBlocks даёт D.

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₂₂ = D$$

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₁₂ = B :=
  rfl

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