English
A block matrix formed by B11, B12, B21, B22 multiplied by a row-partitioned matrix fromRows A1, A2 equals a row-partitioned matrix whose top row is B11 A1 + B12 A2 and whose bottom row is B21 A1 + B22 A2.
Русский
Блочная матрица, составленная из B11, B12, B21, B22, умноженная на блочную матрицу с помощью fromRows A1, A2, равна блочной матрице, у которой верхняя строка равна B11 A1 + B12 A2, нижняя — B21 A1 + B22 A2.
LaTeX
$$$ \mathrm{fromBlocks}(B_{11},B_{12},B_{21},B_{22}) \; (\mathrm{fromRows}(A_1,A_2)) = \mathrm{fromRows}(B_{11} A_1 + B_{12} A_2) (B_{21} A_1 + B_{22} A_2) $$$
Lean4
/-- A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix. -/
theorem fromBlocks_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R)
(B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * (fromRows A₁ A₂) = fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂) := by
ext (_ | _) _ <;> simp [mul_apply]
