Theorem Matrix.dotProduct_star_self_pos_iff

Modification history

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