det_nonneg

Mathlib.LinearAlgebra.Matrix.PosDef

URI: https://scilib.ai/kg/mathlib#Matrix.PosSemidef.det_nonneg

← MathLib Explorer

English

If A is positive semidefinite, then det(A) ≥ 0.

Русский

Если матрица A положительно полуопределена, то.det(A) неотрицателен.

LaTeX

$$$\text{PosSemidef}(A) \implies 0 \le \det(A)$$$

Lean4

theorem det_nonneg [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) : 0 ≤ M.det :=
  by
  rw [hM.isHermitian.det_eq_prod_eigenvalues]
  exact Finset.prod_nonneg fun i _ ↦ by simpa using hM.eigenvalues_nonneg i

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

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

Разделы

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

Аффилиация

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