Commit 2026-04-28 22:33 e769f5e6
View on Github →feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball (#36201) An element in a non-unital C⋆-algebra is a projection iff it is an extreme point of the nonnegative closed unit ball. This is from 1.6.2 in Sakai's C⋆-algebras and W⋆-algebras (the proof is different though).