Projections in C⋆-algebras

To show that an element is a star projection in a non-unital C⋆-algebra, it is enough to show that it is idempotent and normal, because self-adjointedness and normality are equivalent for idempotent elements in non-unital C⋆-algebras.

theorem IsIdempotentElem.isSelfAdjoint_iff_isStarNormal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} (hp : IsIdempotentElem p) : IsSelfAdjoint p ↔ IsStarNormal p

An idempotent element in a non-unital C⋆-algebra is self-adjoint iff it is normal.

theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} : IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p

An element in a non-unital C⋆-algebra is a star projection if and only if it is idempotent and normal.