Theorem LinearMap.isPosSemidef_iff_posSemidef_toMatrix

Modification history

2025-10-23 14:48
Mathlib/LinearAlgebra/SesquilinearForm/Star.lean
feat: properties of sesquilinear forms over a star ring (#30274)
Added LinearMap.isPosSemidef_iff_posSemidef_toMatrixView on Github →