Commit 2025-01-10 07:43 d14cbfb7
View on Github →feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) Add a couple of simp lemmas. In a ring, the product of an idempotent and its complement is zero.
feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) Add a couple of simp lemmas. In a ring, the product of an idempotent and its complement is zero.