Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-23 07:51 106f0ac9

View on Github →

feat(ring_theory/noetherian): Finitely generated idempotent ideal is principal. (#15561)

Estimated changes

Modified src/algebra/ring/idempotents.lean

Modified src/ring_theory/noetherian.lean

modified theorem ideal.fg.map

modified def ideal.fg

modified theorem ideal.fg_ker_comp

added theorem ideal.is_idempotent_elem_iff_eq_bot_or_top

added theorem ideal.is_idempotent_elem_iff_of_fg

added theorem submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul