Theorem Submodule.starProjection_inj

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 Submodule.starProjection_injView on Github →