∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] (f : R →+* S) {I : Type u_3} [inst_2 : Fintype I]
  {e : I → R},
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    (∀ (i : I), IsIdempotentElem (e i)) → CompleteOrthogonalIdempotents (⇑f ∘ e) → CompleteOrthogonalIdempotents e