∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  (∀ (i : I), IsIdempotentElem (e i)) →
    (Pairwise fun x1 x2 => e x1 * e x2 = 0) → ∑ i, e i = 1 → CompleteOrthogonalIdempotents e