Commit 2023-05-06 07:33 4a20b63f

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/AssociatedPrime.lean

added theorem AssociatePrimes.mem_iff

added theorem IsAssociatedPrime.annihilator_le

added theorem IsAssociatedPrime.eq_radical

added theorem IsAssociatedPrime.isPrime

added theorem IsAssociatedPrime.map_of_injective

added def IsAssociatedPrime

added theorem LinearEquiv.AssociatedPrimes.eq

added theorem LinearEquiv.isAssociatedPrime_iff

added theorem associatedPrimes.eq_empty_of_subsingleton

added theorem associatedPrimes.eq_singleton_of_isPrimary

added theorem associatedPrimes.nonempty

added theorem associatedPrimes.subset_of_injective

added def associatedPrimes

added theorem exists_le_isAssociatedPrime_of_isNoetherianRing

added theorem not_isAssociatedPrime_of_subsingleton