Commit 2025-07-31 05:15 e5b94b53

feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections (#25910) This allows us to use subtraction with idempotents and star projections. For idempotents p,q, q - p is idempotent when p * q = p = q * p. For star projections p,q, q - p is a star projection when either p * q = p or q * p = p. In a star-ordered ring, when p * q = p or q * p = p we get p ≤ q.