posDef_diagonal_iff — Mathlib

English

Equivalence for diagonal matrices: PosDef(diagonal(d)) iff ∀ i, d_i > 0.

Русский

Эквивалентность для диагональных матриц: PosDef(diagonal(d)) ⇔ ∀ i, d_i > 0.

LaTeX

$$PosDef( diagonal(d) ) ↔ ∀ i, 0 < d_i$$

Lean4

@[simp]
theorem _root_.Matrix.posDef_diagonal_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nontrivial R]
    {d : n → R} : PosDef (diagonal d) ↔ ∀ i, 0 < d i :=
  by
  refine ⟨fun h i => ?_, .diagonal⟩
  have := h.2 (Pi.single i 1)
  simp_rw [mulVec_single_one, ← Pi.single_star, star_one, single_dotProduct, one_mul, col_apply, diagonal_apply_eq,
    Function.ne_iff] at this
  exact this ⟨i, by simp⟩

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