fromBlocks_toBlocks — Mathlib

English

Given a matrix M with sum-type indices, recomposing from its blocks recovers M.

Русский

Дана матрица M с индексами сумм типа; восстановление M по её блочным частям возвращает исходную матрицу.

LaTeX

$$fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M$$

Lean4

theorem fromBlocks_toBlocks (M : Matrix (n ⊕ o) (l ⊕ m) α) :
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M :=
  by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

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