diagonal_apply_eq

Mathlib.Data.Matrix.Diagonal

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

English

The i,i entry of the diagonal matrix diag(d) is d(i).

Русский

Элемент на позиции i,i диагональной матрицы diag(d) равен d(i).

LaTeX

$$$(\\mathrm{diagonal\\ } d)_{ii} = d(i)$$$

Lean4

@[simp]
theorem diagonal_apply_eq [Zero α] (d : n → α) (i : n) : (diagonal d) i i = d i := by simp [diagonal]

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

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

Разделы

Аффилиация

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