Theorem Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical

Modification history

2026-03-04 10:55
Mathlib/RingTheory/Lasker.lean
feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition (#35599) …
Deleted Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radicalView on Github →
2026-02-10 09:04
Mathlib/RingTheory/Lasker.lean
feat(RingTheory/Lasker): minimal primes arise in any primary decomposition (#34700) …
Added Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radicalView on Github →