mathlib3 documentation

ring_theory.ideal.idempotent_fg

Lemmas on idempotent finitely generated ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A finitely generated idempotent ideal is generated by an idempotent element