Theorem Ideal.exists_le_prime_nmem_of_isIdempotentElem

Modification history