single_mulVec — Mathlib

English

Left multiplying a matrix unit by a vector x yields a vector that is zero everywhere except at index i, where its value is c · x_j.

Русский

Левое умножение единичной матрицей на вектор x даёт вектор, нулевой во всех позициях, кроме i-й, где стоит c · x_j.

LaTeX

$$$ (\mathrm{single}_{i j} c) \cdot x = \mathrm{update} (0 : n \to α) i (c \cdot x_j) $$$

Lean4

theorem single_mulVec [NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : m → α) :
    mulVec (single i j c) x = Function.update (0 : n → α) i (c * x j) :=
  by
  ext i'
  simp [single, mulVec, dotProduct]
  rcases eq_or_ne i i' with rfl | h
  · simp
  simp [h, h.symm]

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