Commit 2024-08-23 12:36 faaca26a

View on Github →

chore(Idempotents): use Pairwise (#15260) Also generalize a few lemmas from [Fintype I] to {s : Finset I}.

Estimated changes

Modified Mathlib/RingTheory/Idempotents.lean

modified theorem CompleteOrthogonalIdempotents.prod_one_sub

modified theorem OrthogonalIdempotents.isIdempotentElem_sum

added theorem OrthogonalIdempotents.mul_sum_of_mem

added theorem OrthogonalIdempotents.mul_sum_of_not_mem

modified theorem OrthogonalIdempotents.prod_one_sub