Theorem LinearMap.IsSymmetricProjection.isPositive

Modification history

2025-10-18 20:17

Mathlib/Analysis/InnerProductSpace/Positive.lean

feat(Analysis/InnerProductSpace/Positive): `U.starProjection ≤ V.starProjection` iff `U ≤ V` (#27162) …

Added LinearMap.IsSymmetricProjection.isPositive View on Github →