English
Let DecidableEq l, Fintype m and NonUnitalNonAssocSemiring α hold. For A ∈ Matrix l m α, i ∈ l, r: m → α and B ∈ Matrix m n α, we have A.updateRow i r * B = (A * B).updateRow i (r ᵥ* B).
Русский
Пусть существуют выбор основания и т.д. Тогда произведение обновлённой строки A на B равняется обновлению произведения A на B, где обновленная строка вычисляется как r ᵥ* B.
LaTeX
$$$A.updateRow(i, r) * B = (A * B).updateRow(i, r \\; ᵥ*\\; B).$$$
Lean4
theorem updateRow_mul [DecidableEq l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l) (r : m → α)
(B : Matrix m n α) : A.updateRow i r * B = (A * B).updateRow i (r ᵥ* B) :=
by
ext i' j'
obtain rfl | hi := eq_or_ne i' i
· simp [mul_apply, vecMul, dotProduct]
· simp [mul_apply, hi]
