Theorem Matrix.posDef_diagonal_iff

Modification history

2024-08-12 23:05
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat: `Matrix.PosDef` on diagonal and numeric matrices (#13974) …
Added Matrix.posDef_diagonal_iffView on Github →