isStarProjection_iff_isIdempotentElem_and_isStarNormal

English

A star projection p satisfies p^2 = p and p^* = p; this holds iff p is idempotent and normal.

Русский

Звездная проекция p имеет p^2 = p и p^* = p; это эквивалентно pIdempotent и нормальности.

LaTeX

$$$$\text{IsStarProjection}(p) \iff (\text{IsIdempotentElem}(p) \wedge \text{IsStarNormal}(p)).$$$$

Lean4

/-- An element in a non-unital C⋆-algebra is a star projection
if and only if it is idempotent and normal. -/
theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal {p : A} :
    IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p :=
  (isStarProjection_iff p).eq ▸ and_congr_right_iff.eq ▸ fun h => h.isSelfAdjoint_iff_isStarNormal

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