Commit 2025-09-09 13:02 d7dfaf98

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem Matrix.isPositive_toEuclideanLin_iff

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self