transpose

Mathlib.LinearAlgebra.Matrix.PosDef

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

← MathLib Explorer

English

If M is PosDef, then its transpose M^T is PosDef.

Русский

Если MPosDef, то M^T также PosDef.

LaTeX

$$PosDef(M) ⇒ PosDef(M^T)$$

Lean4

theorem transpose {M : Matrix n n R'} (hM : M.PosDef) : Mᵀ.PosDef :=
  by
  refine ⟨IsHermitian.transpose hM.1, fun x hx => ?_⟩
  convert hM.2 (star x) (star_ne_zero.2 hx) using 1
  rw [mulVec_transpose, dotProduct_mulVec, star_star, dotProduct_comm]

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

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

Разделы

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

Аффилиация

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