Theorem OrthogonalIdempotents.mul_sum_of_not_mem

Modification history

2024-08-23 12:36
Mathlib/RingTheory/Idempotents.lean
chore(Idempotents): use `Pairwise` (#15260) …
Added OrthogonalIdempotents.mul_sum_of_not_memView on Github →