English
Let A1, A2 be m1×n and m2×n matrices over a semiring, and B1, B2 be n×n1 and n×n2 matrices. Then the row-block matrix formed by A1, A2 multiplied by the column-block matrix formed by B1, B2 is the 2×2 block matrix whose blocks are A1 B1, A1 B2, A2 B1, A2 B2.
Русский
Пусть A1, A2 — матрицы размерности m1×n и m2×n, над полем семирения, а B1, B2 — матрицы размерности n×n1 и n×n2. Тогда блочная матрица из A1, A2 слева умножается на блочную матрицу из B1, B2 справа и получается блочная матрица 2×2 с блоками A1 B1, A1 B2, A2 B1, A2 B2.
LaTeX
$$$ (\mathrm{fromRows}(A_1,A_2))\; (\mathrm{fromCols}(B_1,B_2)) = \mathrm{fromBlocks}(A_1 B_1) (A_1 B_2) (A_2 B_1) (A_2 B_2) $$$
Lean4
/-- A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block
matrix. -/
theorem fromRows_mul_fromCols [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R)
(B₂ : Matrix n n₂ R) : (fromRows A₁ A₂) * (fromCols B₁ B₂) = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) :=
by ext (_ | _) (_ | _) <;> simp
