Theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing

Modification history