English
Let p be a row predicate, q a column predicate, A,B be matrices with entries in a ring, and r a third predicate on rows. The block of AB corresponding to p,r equals the block products plus a second block product with the complement of q: (A B).toBlock p r = A.toBlock p q · B.toBlock q r + A.toBlock p (λ i, ¬ q i) · B.toBlock (λ i, ¬ q i) r.
Русский
Пусть p — предикат на строки, q — на столбцы, A,B — матрицы над кольцом, и r — предикат на строки. Блок AB, соответствующий p,r, равен произведению блоков A и B по q и r плюс произведению по комплименту q: (AB).toBlock p r = A.toBlock p q · B.toBlock q r + A.toBlock p (λ i, ¬ q i) · B.toBlock (λ i, ¬ q i) r.
LaTeX
$$$(A B).toBlock p r = A.toBlock p q \\cdot B.toBlock q r + A.toBlock p (fun i => \\neg q i) \\cdot B.toBlock (fun i => \\neg q i) r$$$
Lean4
theorem toBlock_mul_eq_add {m n k : Type*} [Fintype n] (p : m → Prop) (q : n → Prop) [DecidablePred q] (r : k → Prop)
(A : Matrix m n R) (B : Matrix n k R) :
(A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r :=
by
classical
ext i k
simp only [toBlock_apply, mul_apply]
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm
