Commit 2025-04-23 09:49 4790a8f3

View on Github →

chore(RingTheory/Ideal): move associated prime (#23876) Move associated prime into a folder for further developments.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime.lean

deleted theorem AssociatePrimes.mem_iff

deleted theorem IsAssociatedPrime.annihilator_le

deleted theorem IsAssociatedPrime.eq_radical

deleted theorem IsAssociatedPrime.isPrime

deleted theorem IsAssociatedPrime.map_of_injective

deleted def IsAssociatedPrime

deleted theorem LinearEquiv.AssociatedPrimes.eq

deleted theorem LinearEquiv.isAssociatedPrime_iff

deleted theorem associatedPrimes.eq_empty_of_subsingleton

deleted theorem associatedPrimes.eq_singleton_of_isPrimary

deleted theorem associatedPrimes.nonempty

deleted theorem associatedPrimes.subset_of_injective

deleted def associatedPrimes

deleted theorem biUnion_associatedPrimes_eq_zero_divisors

deleted theorem exists_le_isAssociatedPrime_of_isNoetherianRing

deleted theorem not_isAssociatedPrime_of_subsingleton

Created Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.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 biUnion_associatedPrimes_eq_zero_divisors

added theorem exists_le_isAssociatedPrime_of_isNoetherianRing

added theorem not_isAssociatedPrime_of_subsingleton

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean