Theorem Matrix.PosDef.dotProduct_mulVec_pos

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.dotProduct_mulVec_posView on Github →