Theorem isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star

Modification history

2026-03-10 21:33
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean
feat(Analysis/CStarAlgebra): `IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}` (#35916) …
Added isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_starView on Github →