isSymmetricProjection_starProjection

English

The star projection is a symmetric projection.

Русский

Звёздочная проекция является симметричной проекцией.

LaTeX

$$$ U.starProjection.IsSymmetricProjection. $$$

Lean4

/-- `U.starProjection` is a symmetric projection. -/
@[simp]
theorem isSymmetricProjection_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
    U.starProjection.IsSymmetricProjection :=
  ⟨U.isIdempotentElem_starProjection.toLinearMap, U.starProjection_isSymmetric⟩

Похожие утверждения