Commit 2025-01-20 15:06 f033341c

View on Github →

feat(RingTheory): minimal primes are contained in zero divisors (#20306)

Estimated changes

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

added theorem Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes

added theorem Ideal.exists_mul_mem_of_mem_minimalPrimes

added theorem Ideal.iUnion_minimalPrimes