posSemidef_diagonal_iff — Mathlib

English

A diagonal matrix diag(d) is positive semidefinite if and only if every diagonal entry d(i) is nonnegative.

Русский

Диагональная матрица diag(d) положительно полуположна тогда и только тогда, когда каждый диагональный элемент d(i) неотрицателен.

LaTeX

$$$\mathrm{PosSemidef}(\mathrm{diagonal}(d)) \iff \forall i,\ 0 \le d(i)$$$

Lean4

/-- A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative. -/
theorem posSemidef_diagonal_iff [StarOrderedRing R] [DecidableEq n] {d : n → R} :
    PosSemidef (diagonal d) ↔ (∀ i : n, 0 ≤ d i) :=
  ⟨fun ⟨_, hP⟩ i ↦ by simpa using hP (Pi.single i 1), .diagonal⟩

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