Theorem associatedPrimes.nonempty

Modification history

2025-04-23 09:49

Mathlib/RingTheory/Ideal/AssociatedPrime.lean

chore(RingTheory/Ideal): move associated prime (#23876) …

Modified associatedPrimes.nonempty View on Github →

2023-05-06 07:33

Mathlib/RingTheory/Ideal/AssociatedPrime.lean

feat port : RingTheory.Ideal.AssociatedPrime (#3810)

Added associatedPrimes.nonempty View on Github →