Lemmas on idempotent finitely generated ideals

theorem Ideal.isIdempotentElem_iff_of_fg {R : Type u_1} [CommRing R] (I : Ideal R) (h : Ideal.FG I) : IsIdempotentElem I ↔ ∃ (e : R), IsIdempotentElem e ∧ I = Submodule.span R {e}

A finitely generated idempotent ideal is generated by an idempotent element

theorem Ideal.isIdempotentElem_iff_eq_bot_or_top {R : Type u_1} [CommRing R] [IsDomain R] (I : Ideal R) (h : Ideal.FG I) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤