natCast — Mathlib

English

A diagonal matrix with a nonnegative natural scalar on the diagonal is PSD.

Русский

Диагональная матрица с неотрицательным натуральным числом на диагонали ПСД.

LaTeX

$$$\mathrm{PosSemidef}((d) I) \quad (d \ge 0,\ d \in \mathbb{N})$$$

Lean4

protected theorem natCast [StarOrderedRing R] [DecidableEq n] (d : ℕ) : PosSemidef (d : Matrix n n R) :=
  ⟨isHermitian_natCast _, fun x =>
    by
    rw [natCast_mulVec, Nat.cast_smul_eq_nsmul, dotProduct_smul]
    exact nsmul_nonneg (dotProduct_star_self_nonneg _) _⟩

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