Commit 2025-10-12 11:37 c4b611e4

View on Github →

feat(LinearAlgebra/Matrix/PosDef): vecMulVec a (star a) is positive semi-definite (#29861) The matrices vecMulVec a (star a) and vecMulVec (star a) a are always positive semi-definite.

Estimated changes

Modified Mathlib/Data/Matrix/Mul.lean

added theorem exists_ne_zero_dotProduct_eq_zero

added theorem not_injective_dotProduct_left

added theorem not_injective_dotProduct_right

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.PosDef.mul_conjTranspose_self

added theorem Matrix.posSemidef_vecMulVec_self_star

added theorem Matrix.posSemidef_vecMulVec_star_self