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 _ _ _