Theorem Matrix.isPositive_toEuclideanLin_iff

Modification history

2025-09-09 13:02

Mathlib/Analysis/InnerProductSpace/Positive.lean

feat(Analysis/InnerProductSpace/Positive): `A.toEuclideanLin.IsPositive` iff `A.PosSemidef` (#28553)

Added Matrix.isPositive_toEuclideanLin_iff View on Github →