Theorem Ideal.exists_mul_mem_of_mem_minimalPrimes

Modification history

2025-01-20 15:06
Mathlib/RingTheory/Ideal/MinimalPrime.lean
feat(RingTheory): minimal primes are contained in zero divisors (#20306)
Added Ideal.exists_mul_mem_of_mem_minimalPrimesView on Github →