Theorem Matrix.posSemidef_vecMulVec_star_self

Modification history

2025-10-12 11:37
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat(LinearAlgebra/Matrix/PosDef): `vecMulVec a (star a)` is positive semi-definite (#29861) …
Added Matrix.posSemidef_vecMulVec_star_selfView on Github →