Theorem: Matrix.PosSemidef_zero (CvxLean/Lib/Math/LogDet.lean)

State before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
⊢ PosSemidef 0
Tactic:
simp [PosSemidef]
State after:
no goals