updateRow_mulVec — Mathlib

English

The i-th row after an update by c, multiplied by a vector v, equals updating the product A·v at index i by the dot product c with v.

Русский

Строка i после обновления коэффициентами c, умноженная на вектор v, равна обновлению произведения A·v в координате i на скалярную двойку c и v.

LaTeX

$$$A.\text{updateRow } i\, c \; *\ᵥ\; v = \text{Function.update} (A \*ᵥ v)\, i\ (c \; ⬝ᵥ\; v)$$$

Lean4

theorem updateRow_mulVec [DecidableEq l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l)
    (c : m → α) (v : m → α) : A.updateRow i c *ᵥ v = Function.update (A *ᵥ v) i (c ⬝ᵥ v) :=
  by
  ext i'
  obtain rfl | hi := eq_or_ne i' i
  · simp [mulVec]
  · simp [mulVec, hi]

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