Theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal

Modification history

2025-07-26 16:23
Mathlib/Analysis/CStarAlgebra/Projection.lean
feat(Analysis/CStarAlgebra/...): an idempotent element in a C*-algebra is self-adjoint iff it is normal (#27475)
Added isStarProjection_iff_isIdempotentElem_and_isStarNormalView on Github →