English
Let p be a predicate on rows and q a predicate on columns. For A ∈ Matrix m×n R and B ∈ Matrix n×k R, the (p,q)-block of AB equals the product of the corresponding blocks: (AB).toBlock p q = A.toBlock p ⊤ · B.toBlock ⊤ q.
Русский
Пусть p задано на строки, q — на столбцы. Для матриц A (m×n) и B (n×k) над кольцом R, блок-матрица AB, относящаяся к p и q, равна произведению соответствующих блоков: (AB).toBlock p q = A.toBlock p ⊤ · B.toBlock ⊤ q.
LaTeX
$$$(A B)^{\\mathrm{toBlock}}_{p q} = A^{\\mathrm{toBlock}}_{p \\top} \\cdot B^{\\mathrm{toBlock}}_{\\top q}$$$
Lean4
theorem toBlock_mul_eq_mul {m n k : Type*} [Fintype n] (p : m → Prop) (q : k → Prop) (A : Matrix m n R)
(B : Matrix n k R) : (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q :=
by
ext i k
simp only [toBlock_apply, mul_apply]
rw [Finset.sum_subtype]
simp [Pi.top_apply, «Prop».top_eq_true]
