Theorem associatedPrimes.subset_of_injective

Modification history

2025-05-01 08:12
Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
feat(RingTheory/Ideal/AssociatedPrime/Basic): associated primes and exact sequence (#24453) …
Modified associatedPrimes.subset_of_injectiveView on Github →
2025-04-23 09:49
Mathlib/RingTheory/Ideal/AssociatedPrime.lean
chore(RingTheory/Ideal): move associated prime (#23876) …
Modified associatedPrimes.subset_of_injectiveView on Github →
2023-05-06 07:33
Mathlib/RingTheory/Ideal/AssociatedPrime.lean
feat port : RingTheory.Ideal.AssociatedPrime (#3810)
Added associatedPrimes.subset_of_injectiveView on Github →