Theorem LinearMap.IsSymmetricProjection.sub_of_range_le_range

Modification history

2025-10-18 20:17
Mathlib/Analysis/InnerProductSpace/Symmetric.lean
feat(Analysis/InnerProductSpace/Positive): `U.starProjection ≤ V.starProjection` iff `U ≤ V` (#27162) …
Added LinearMap.IsSymmetricProjection.sub_of_range_le_rangeView on Github →