Theorems · Definition · linear algebra

Matrix.PosDef

{n : Type u_2} → {R : Type u_3} → [inst : Ring R] → [PartialOrder R] → [StarRing R] → Matrix n n R → Prop

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

68 results in Mathlib

Foundations

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

Assumes

RingPartialOrderStarRing