Theorem Ideal.disjoint_nonZeroDivisors_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.disjoint_nonZeroDivisors_of_mem_minimalPrimesView on Github →