Theorem Matrix.posDef_iff_dotProduct_mulVec

Modification history

2025-12-09 04:22
Mathlib/LinearAlgebra/Matrix/PosDef.lean
refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)
Added Matrix.posDef_iff_dotProduct_mulVecView on Github →