English
The star projection operator is a positive operator; in particular, it is idempotent and self-adjoint.
Русский
Оператор starProjection является положительным; он идемпотентен и самопряжён.
LaTeX
$$starProjection (U) is positive$$
Lean4
/-- The orthogonal projection onto a subspace as a map from the full space to itself,
as opposed to `Submodule.orthogonalProjection`, which maps into the subtype. This
version is important as it satisfies `IsStarProjection`. -/
def starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : E →L[𝕜] E :=
U.subtypeL ∘L U.orthogonalProjection