Theorem Matrix.dotProduct_self_star_pos_iff

Modification history

2026-09-30 15:24
Mathlib/LinearAlgebra/Matrix/DotProduct.lean
feat(Algebra/Star/Basic): class for `star x * x = 0 → x = 0` (#44080) …
Modified Matrix.dotProduct_self_star_pos_iffView on Github →
2024-08-12 23:05
Mathlib/LinearAlgebra/Matrix/DotProduct.lean
feat: `Matrix.PosDef` on diagonal and numeric matrices (#13974) …
Added Matrix.dotProduct_self_star_pos_iffView on Github →