diagonal_neg

Mathlib.Data.Matrix.Diagonal

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

English

Negation commutes with forming a diagonal matrix.

Русский

Отрицание commute c построением диагональной матрицы.

LaTeX

$$$-\\mathrm{diag}(d) = \\mathrm{diag}(-d)$$$

Lean4

@[simp]
theorem diagonal_neg [NegZeroClass α] (d : n → α) : -diagonal d = diagonal fun i => -d i :=
  by
  ext i j
  by_cases h : i = j <;> simp [h]

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

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

Разделы

Аффилиация

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