Theorem Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff

Modification history

2026-02-24 15:42
Mathlib/RingTheory/Lasker.lean
refactor(RingTheory/Ideal/AssociatedPrime/Basic): redefine associated primes to include a radical (#34221) …
Deleted Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iffView on Github →
2026-02-21 11:43
Mathlib/RingTheory/Lasker.lean
feat(RingTheory/Lasker): prove first uniqueness theorem for primary decomposition (#34699) …
Added Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iffView on Github →