transpose_iff

Mathlib.LinearAlgebra.Matrix.PosDef

URI: https://scilib.ai/kg/mathlib#Matrix.PosDef.transpose_iff

English

M^T is PosDef iff M is PosDef.

Русский

M^TPosDef ⇔ M PosDef.

LaTeX

$$PosDef(M^T) ↔ PosDef(M)$$

Lean4

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

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

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

Разделы

Аффилиация

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