Theorems · Theorem · linear algebra

Matrix.PosDef.dotProduct_mulVec_pos

∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.PosDef → ∀ {x : n → R}, x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x

A matrix M : Matrix n n R is positive definite if it is Hermitian and xᴴMx is greater than zero for all nonzero x.

Defined in

Mathlib.LinearAlgebra.Matrix.PosDef

Cited by

7 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingPartialOrderStarRingFintype