Theorem not_injective_dotProduct_left

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 not_injective_dotProduct_leftView on Github →