Commit 2025-07-28 21:07 554c34a2
View on Github →feat(Analysis/InnerProductSpace/Positive.): add theorem LinearMap.IsPositive.of_isStarProjection (#27246)
This two theorems where already added for ContinuousLinearMap, and in this pull request I'm adding them for LinearMap