English
For A ∈ M_{l×m}(α), i ∈ {1,...,m}, j ∈ {1,...,n}, and r ∈ α, the product A·single i j r equals updateCol 0 j (A.col i <• r). This expresses how multiplying A by a matrix that alters column j on the right corresponds to scaling of the i-th column of A.
Русский
Для A ∈ M_{l×m}(α), i в диапазоне столбцов, j в диапазоне столбцов B, и r ∈ α, произведение A·single i j r равно updateCol 0 j (A.col i • r).
LaTeX
$$$\forall A\in M_{l,m},\; i\in m,\; j\in n,\; r\in α:\quad A \cdot \text{single } i j r = \text{updateCol } 0 j (A.col i \; <•\; r)$. $$
Lean4
theorem mul_single_eq_updateCol_zero [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α]
(A : Matrix l m α) (i : m) (j : n) (r : α) : A * single i j r = updateCol 0 j (A.col i <• r) := by
rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_single]
