English
Let A1, A2 be m1×n and m2×n matrices, and B1, B2 be n×n1 and n×n2 matrices. Then the product fromCols A1 A2 times fromRows B1 B2 equals the sum of outer products A1 B1 and A2 B2, i.e., A1 B1 + A2 B2.
Русский
Пусть A1, A2 — матрицы размерности m1×n и m2×n, а B1, B2 — матрицы размера n×n1 и n×n2. Тогда произведение fromCols A1 A2 на fromRows B1 B2 равно сумме внешних произведений A1 B1 и A2 B2: A1 B1 + A2 B2.
LaTeX
$$$ \mathrm{fromCols}(A_1,A_2) \cdot \mathrm{fromRows}(B_1,B_2) = A_1 B_1 + A_2 B_2 $$$
Lean4
/-- A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer"
products of the block matrices. -/
theorem fromCols_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R)
(B₂ : Matrix n₂ n R) : fromCols A₁ A₂ * fromRows B₁ B₂ = (A₁ * B₁ + A₂ * B₂) :=
by
ext
simp [mul_apply]
