English
The i-th column of the diagonal matrix diag(d) is the vector with i at position i and zeros elsewhere, i.e., Pi.single i (d(i)).
Русский
i-я колонка диагональной матрицы diag(d) есть вектор, у которого на позиции i стоит d(i), а остальные нули; это Pi.single i (d(i)).
LaTeX
$$$\mathrm{diag}(d).\mathrm{col} \, i = \mathrm{Pi}.\mathrm{single}\, i \, (d(i))$$$
Lean4
@[simp]
theorem col_diagonal [Zero α] (d : n → α) (i) : (diagonal d).col i = Pi.single i (d i) :=
by
ext
simp +contextual [diagonal, Pi.single_apply]