Theorem ContinuousLinearMap.IsPositive.of_isStarPojection

Modification history

2025-07-13 18:42
Mathlib/Analysis/InnerProductSpace/Positive.lean
chore(Analysis/InnerProductSpace/Positive): typo (#27078)
Deleted ContinuousLinearMap.IsPositive.of_isStarPojectionView on Github →
2025-07-10 20:17
Mathlib/Analysis/InnerProductSpace/Positive.lean
feat(Analysis/InnerProductSpace/Positive): a star projection operator is positive (#26631) …
Added ContinuousLinearMap.IsPositive.of_isStarPojectionView on Github →