posSemidef_transpose_iff

Mathlib.LinearAlgebra.Matrix.PosDef

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

← MathLib Explorer

English

A matrix M is PSD if and only if its transpose M^T is PSD.

Русский

Матрица M ПСД тогда и только тогда, когда M^T ПСД.

LaTeX

$$$\text{PosSemidef}(M^T) \iff \text{PosSemidef}(M)$$$

Lean4

@[simp]
theorem _root_.Matrix.posSemidef_transpose_iff {M : Matrix n n R'} : Mᵀ.PosSemidef ↔ M.PosSemidef :=
  ⟨(by simpa using ·.transpose), .transpose⟩

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

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

Разделы

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

Аффилиация

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