Theorems · Theorem · linear algebra

Matrix.PosSemidef.dotProduct_mulVec_zero_iff

∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] {A : Matrix n n 𝕜},
  A.PosSemidef → ∀ (x : n → 𝕜), star x ⬝ᵥ A.mulVec x = 0 ↔ A.mulVec x = 0

For A positive semidefinite, we have x⋆ A x = 0 iff A x = 0.

Defined in

Mathlib.Analysis.Matrix.Order

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeFintype