diagonal_transpose

Mathlib.Data.Matrix.Diagonal

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

← MathLib Explorer

English

The diagonal matrix is equal to its transpose.

Русский

Диагональная матрица равна своей транспонированной.

LaTeX

$$$\\mathrm{diag}(v)^{\\top} = \\mathrm{diag}(v)$$$

Lean4

@[simp]
theorem diagonal_transpose [Zero α] (v : n → α) : (diagonal v)ᵀ = diagonal v :=
  by
  ext i j
  by_cases h : i = j
  · simp [h, transpose]
  · simp [h, transpose, diagonal_apply_ne' _ h]

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

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

Разделы

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

Аффилиация

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