Commit 2025-07-27 22:37 c3f51d41

feat(Analysis/InnerProductSpace/Adjoint): a normal idempotent operator is a star projection (#26767) This adds that an idempotent operator is self-adjoint if and only if it is normal. This means that a normal idempotent operator is a star projection. Along with #26631, we get that for idempotent operators, normality, self-adjointedness, and positivity are all equivalent.