row_diagonal

Mathlib.Data.Matrix.Diagonal

URI: https://scilib.ai/kg/mathlib#Matrix.row_diagonal

← MathLib Explorer

English

Similarly, the i-th row of diag(d) is Pi.single i (d(i)).

Русский

Аналогично, i-я строка diag(d) равна Pi.single i (d(i)).

LaTeX

$$$\mathrm{diag}(d).\mathrm{row} \, i = \mathrm{Pi}.\mathrm{single}\, i \, (d(i))$$$

Lean4

@[simp]
theorem row_diagonal [Zero α] (d : n → α) (j) : (diagonal d).row j = Pi.single j (d j) :=
  by
  ext
  simp +contextual [diagonal, eq_comm, Pi.single_apply]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru