fromCols_fromRows_eq_fromBlocks — Mathlib

English

Combining left and right row-blocks and then taking columns equals the full block matrix. Specifically, fromCols(fromRows(B11,B21), fromRows(B12,B22)) = fromBlocks(B11,B12,B21,B22).

Русский

Соединяя слева-право блоки по строкам и затем беря столбцы, получим исходную блочную матрицу: fromCols(fromRows(B11,B21), fromRows(B12,B22)) = fromBlocks(B11,B12,B21,B22).

LaTeX

$$$$ \operatorname{fromCols}(\operatorname{fromRows}(B_{11},B_{21}), \operatorname{fromRows}(B_{12},B_{22})) = \operatorname{fromBlocks}(B_{11},B_{12},B_{21},B_{22}). $$$$

Lean4

@[simp]
theorem fromCols_fromRows_eq_fromBlocks (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R)
    (B₂₂ : Matrix m₂ n₂ R) : fromCols (fromRows B₁₁ B₂₁) (fromRows B₁₂ B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ := by
  ext (_ | _) (_ | _) <;> simp

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