English
For zero blocks in the outer blocks, the product (0).updateRow i r · (0).updateCol j c evaluates to a single rank-one update: it equals single i j (r ⬝ᵥ c).
Русский
При нулевых внешних блоках произведение $(0).updateRow_i(r) \cdot (0).updateCol_j(c)$ равно единичной ранговой обновляющей матрице: $\\text{single } i j (r \\; ⬝ᵥ\\; c)$.
LaTeX
$$$\\bigl(0_{l\\times m}.updateRow i r\\bigr)\\; \\bigl(0_{m\\times n}.updateCol j c\\bigr) = \\text{single } i j (r \\; ⬝ᵥ\\; c)$$$
Lean4
@[simp]
theorem updateRow_zero_mul_updateCol_zero [DecidableEq l] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α]
(i : l) (r : m → α) (j : n) (c : m → α) :
(0 : Matrix l m α).updateRow i r * (0 : Matrix m n α).updateCol j c = single i j (r ⬝ᵥ c) := by
rw [updateRow_mul, vecMul_updateCol, mul_updateCol, single_eq_of_single_single, Matrix.zero_mul, vecMul_zero,
zero_mulVec, updateCol_zero_zero, updateRow, ← Pi.single, ← Pi.single]
