Continuous functional caculus and projections

This file collects some results related to projections, idempotents, and the continuous functional calculus.

theorem isIdempotentElem_iff_quasispectrum_subset (R : Type u_1) {A : Type u_2} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p] (a : A) (ha : p a) : IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}

theorem isIdempotentElem_iff_spectrum_subset (R : Type u_1) {A : Type u_2} {p : A → Prop} [Field R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [NonUnitalContinuousFunctionalCalculus R A p] (a : A) (ha : p a) : IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}

theorem isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {x : A} : IsIdempotentElem (star x * x) ↔ IsIdempotentElem (x * star x)