single_eq_updateRow_zero — Mathlib

English

A matrix with a single nonzero entry can be obtained by updating a zero matrix at a single row from a one-sparse row vector.

Русский

Матрица, имеющая единственный ненулевой элемент, получается как обновление нулевой матрицы по одной строке, используя одномерный вектор.

LaTeX

$$$\mathrm{single}\ i\ j\ r = \mathrm{updateRow}\ 0\ i\ (\mathrm{Pi.single}_{j} r)$$$

Lean4

theorem single_eq_updateRow_zero [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (r : α) :
    single i j r = updateRow 0 i (Pi.single j r) :=
  single_eq_of_single_single _ _ _

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