Commit 2025-01-10 20:46 3949513a

feat(Order): Boolean algebra structure on idempotents (#20618) We show that the idempotent in a commutative ring form a Boolean algebra, with complement given by a ↦ 1 - a and infimum given by multiplication. In a commutative semiring where subtraction is not available, it is still true that pairs of elements (a, b) satisfying a * b = 0 and a + b = 1 form a Boolean algebra (such elements are automatically idempotents, and such a pair is uniquely determined by either a or b).