Documentation

Mathlib.RingTheory.Ideal.IdempotentFG

Lemmas on idempotent finitely generated ideals #

A finitely generated idempotent ideal is generated by an idempotent element