single — Mathlib

English

single i j a is the matrix with a in the (i,j) position and zeros elsewhere.

Русский

matrix с одним элементом a в позиции (i,j) и нулями в остальных позициях.

LaTeX

$$$\text{single}(i,j,a) = \text{the matrix with } a \text{ at } (i,j) \text{ and zeros elsewhere}.$$$

Lean4

/-- `single i j a` is the matrix with `a` in the `i`-th row, `j`-th column,
and zeroes elsewhere.
-/
def single (i : m) (j : n) (a : α) : Matrix m n α :=
  of <| fun i' j' => if i = i' ∧ j = j' then a else 0

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