single_mul_eq_updateRow_zero — Mathlib

English

Let i ∈ l and j ∈ m with r ∈ α^m, B ∈ M_{m×n}(α). Then single i j r · B = updateRow 0 i (r • B.row j). This describes how left-multiplication by a single row block interacts with a row update.

Русский

Пусть i ∈ l, j ∈ m, r ∈ α, B ∈ M_{m×n}(α). Тогда single i j r · B = updateRow 0 i (r • B.row j).

LaTeX

$$$\text{single } i j r \; B = \text{updateRow } 0\ i\ (r \cdot B_{j})$$$

Lean4

theorem single_mul_eq_updateRow_zero [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (i : l)
    (j : m) (r : α) (B : Matrix m n α) : single i j r * B = updateRow 0 i (r • B.row j) := by
  rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]

Похожие утверждения