diagonal — Mathlib

English

If a matrix M is positive semidefinite, then M is Hermitian.

Русский

Если матрица M положительно полуопределена, то она эрмитова.

LaTeX

$$$M \text{posSemidef} \ \Rightarrow\ M \text{IsHermitian}$$$

Lean4

protected theorem diagonal [StarOrderedRing R] [DecidableEq n] {d : n → R} (h : 0 ≤ d) : PosSemidef (diagonal d) :=
  ⟨isHermitian_diagonal_of_self_adjoint _ <| funext fun i => IsSelfAdjoint.of_nonneg (h i), fun x =>
    by
    refine Fintype.sum_nonneg fun i => ?_
    simpa only [mulVec_diagonal, ← mul_assoc] using conjugate_nonneg (h i) _⟩

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