Commit 2023-08-08 16:37 dc585c91
View on Github →feat: Positivity/Nonnegativity of Eigenvalues of PosDef/PosSemidef Matrices (#6368) Two lemmas:
Matrix.PosDef.eigenvalues_pos: $$A \in k^{n\times n}, A > 0 \implies \lambda (A) >0$$Matrix.PosSemidef.eigenvalues_nonneg: $$A \in k^{n\times n}, A \geq 0 \implies \lambda (A) \geq 0$$