posSemidef_intCast_iff — Mathlib

English

A real-valued interpretation of the integer cast yields PSD if and only if the value is nonnegative.

Русский

Пусть целочисленное отображение задает диагональную матрицу; она PSD тогда и только тогда, когда число неотрицательно.

LaTeX

$$$\text{PosSemidef}(d I) \iff d \ge 0$ для $d \in \mathbb{Z}$$$

Lean4

@[simp]
protected theorem _root_.Matrix.posSemidef_intCast_iff [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R]
    (d : ℤ) : PosSemidef (d : Matrix n n R) ↔ 0 ≤ d :=
  posSemidef_diagonal_iff.trans <| by simp

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