Commit 2026-02-21 11:43 970fe7b9
View on Github →feat(RingTheory/Lasker): prove first uniqueness theorem for primary decomposition (#34699)
This PR proves the first uniqueness theorem for primary decomposition: In any minimal primary decomposition I = ⨅ i, q_i, the ideals √(q_i : M) are exactly the associated primes of I.