Commit 2025-10-18 20:17 c1dddc75

View on Github →

feat(Analysis/InnerProductSpace/Positive): U.starProjection ≤ V.starProjection iff U ≤ V (#27162) For symmetric projections p and q, p ≤ q iff range p ≤ range q, so then: U.starProjection ≤ V.starProjection iff U ≤ V, which implies that Submodule.starProjection is an injective function.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

deleted theorem LinearMap.IsPositive.of_isSymmetricProjection

added theorem LinearMap.IsSymmetricProjection.isPositive

added theorem LinearMap.IsSymmetricProjection.le_iff_range_le_range

added theorem Submodule.starProjection_inj

added theorem Submodule.starProjection_le_starProjection_iff

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

added theorem LinearMap.IsSymmetricProjection.sub_of_range_le_range