Commit 2025-07-10 20:17 d19cd93f
View on Github →feat(Analysis/InnerProductSpace/Positive): a star projection operator is positive (#26631) This shows that a star projection (i.e., a self-adjoint idempotent) operator is positive.
feat(Analysis/InnerProductSpace/Positive): a star projection operator is positive (#26631) This shows that a star projection (i.e., a self-adjoint idempotent) operator is positive.