Theorem Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes

Modification history

2026-03-04 10:55
Mathlib/RingTheory/Lasker.lean
feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition (#35599) …
Modified Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primesView on Github →
2026-02-27 09:51
Mathlib/RingTheory/Lasker.lean
feat: classical "decidability" instances on sets and ideals (#33757) …
Modified Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primesView on Github →
2026-02-24 15:42
Mathlib/RingTheory/Lasker.lean
refactor(RingTheory/Ideal/AssociatedPrime/Basic): redefine associated primes to include a radical (#34221) …
Added Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primesView on Github →