Theorem Matrix.PosSemidef.of_dotProduct_mulVec_nonneg

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