Theorem Matrix.PosDef.mul_conjTranspose_self

Modification history

2026-09-30 15:24
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat(Algebra/Star/Basic): class for `star x * x = 0 → x = 0` (#44080) …
Modified Matrix.PosDef.mul_conjTranspose_selfView on Github →
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.PosDef.mul_conjTranspose_selfView on Github →