Lemmas on idempotent finitely generated ideals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
ideal.is_idempotent_elem_iff_of_fg
{R : Type u_1}
[comm_ring R]
(I : ideal R)
(h : I.fg) :
is_idempotent_elem I ↔ ∃ (e : R), is_idempotent_elem e ∧ I = submodule.span R {e}
A finitely generated idempotent ideal is generated by an idempotent element