posDef_intCast_iff — Mathlib

English

Let d be an integer. The diagonal matrix d I_n is positive definite if and only if d > 0.

Русский

Пусть d целое. Диагональная матрица d I_n положительно определена тогда и только тогда, когда d > 0.

LaTeX

$$$$ \\operatorname{PosDef}(d I_n) \\iff 0 < d. $$$$

Lean4

@[simp]
theorem _root_.Matrix.posDef_intCast_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n]
    [Nontrivial R] {d : ℤ} : PosDef (d : Matrix n n R) ↔ 0 < d :=
  posDef_diagonal_iff.trans <| by simp

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