English
Multiplying a column-assembled matrix by a 2×2 block matrix yields a column-assembled matrix whose blocks are linear combinations of products A1B1 + A2B21 and A1B12 + A2B22.
Русский
Умножение колонки-матрицы на блочную матрицу 2×2 дает матрицу в виде fromCols(A1B11 + A2B21, A1B12 + A2B22).
LaTeX
$$$\big(\mathrm{fromCols}(A_1,A_2)\big) \cdot \mathrm{fromBlocks}(B_{11},B_{12},B_{21},B_{22}) = \mathrm{fromCols}(A_1 B_{11} + A_2 B_{21}, A_1 B_{12} + A_2 B_{22})$$$
Lean4
/-- A column partitioned matrix multipiled by a block matrix results in a column partitioned
matrix. -/
theorem fromCols_mul_fromBlocks [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
(B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
(fromCols A₁ A₂) * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = fromCols (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂) := by
ext _ (_ | _) <;> simp [mul_apply]
