diagonal_apply_ne'

Mathlib.Data.Matrix.Diagonal

URI: https://scilib.ai/kg/mathlib#Matrix.diagonal_apply_ne'

English

If i ≠ j, the entry is zero; diagonal entry is d(i).

Русский

Если i ≠ j, элемент равен нулю; диагональный элемент равен d(i).

LaTeX

$$$i \\neq j \\Rightarrow (\\mathrm{diagonal}\\ d)_{ij} = 0$$$

Lean4

theorem diagonal_apply_ne' [Zero α] (d : n → α) {i j : n} (h : j ≠ i) : (diagonal d) i j = 0 :=
  diagonal_apply_ne d h.symm

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

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

Разделы

Аффилиация

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