posDef_natCast_iff

Mathlib.LinearAlgebra.Matrix.PosDef

URI: https://scilib.ai/kg/mathlib#Matrix.posDef_natCast_iff

← MathLib Explorer

English

For any n, d ∈ ℕ, PosDef(d) ⇔ d > 0.

Русский

Для любого n, d ∈ ℕ, PosDef(d) ⇔ d > 0.

LaTeX

$$PosDef( d ) ⇔ d > 0$$

Lean4

@[simp]
theorem _root_.Matrix.posDef_natCast_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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru