Commit 2026-03-04 10:55 6ad342fe

View on Github →

feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition (#35599) This PR proves the second uniqueness theorem for primary decomposition.

Estimated changes

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean

Modified Mathlib/RingTheory/IsPrimary.lean

Modified Mathlib/RingTheory/Lasker.lean

deleted theorem Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical

added theorem Submodule.IsMinimalPrimaryDecomposition.Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical

added theorem Submodule.IsMinimalPrimaryDecomposition.Submodule.isLasker

added theorem Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf

added theorem Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite

modified theorem Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes

added theorem Submodule.IsMinimalPrimaryDecomposition.injOn

added theorem Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes

deleted theorem Submodule.isLasker