Theorem Matrix.posSemidef_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.posSemidef_iff_dotProduct_mulVec View on Github →