fromRows_fromCols_eq_fromBlocks — Mathlib

English

Similarly, fromRows(fromCols(B11,B12), fromCols(B21,B22)) equals the same fromBlocks(B11,B12,B21,B22).

Русский

Аналогично, fromRows(fromCols(B11,B12), fromCols(B21,B22)) = fromBlocks(B11,B12,B21,B22).

LaTeX

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

Lean4

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

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