Commit 2023-03-19 06:37 730d5981

View on Github →

feat: port RingTheory.Ideal.IdempotentFg (#2980)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/IdempotentFg.lean

added theorem Ideal.isIdempotentElem_iff_eq_bot_or_top

added theorem Ideal.isIdempotentElem_iff_of_fg