col_diagonal — Mathlib

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]

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