Theorem exists_ne_zero_dotProduct_eq_zero

Modification history

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