posSemidef_vecMulVec_self_star

Mathlib.LinearAlgebra.Matrix.PosDef

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

← MathLib Explorer

English

The matrix vecMulVec(a, star a) is always PSD.

Русский

Матрица vecMulVec(a, star a) всегда PSD.

LaTeX

$$(vecMulVec a (star a)).PosSemidef$$

Lean4

/-- The matrix `vecMulVec a (star a)` is always positive semi-definite. -/
theorem posSemidef_vecMulVec_self_star [StarOrderedRing R] (a : n → R) : (vecMulVec a (star a)).PosSemidef := by
  simp [vecMulVec_eq Unit, ← conjTranspose_replicateCol, posSemidef_self_mul_conjTranspose]

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

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

Разделы

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

Аффилиация

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