Primary Decomposition?

Stream: Is there code for X?

[Jack J Garzella]

Has anyone done anything towards primary decomposition of ideals?

In particular, @Calvin Lee and I will want to show the "first uniqueness theorem", or Theorem 4.5 in Atiyah-MacDonald. I couldn't find it in mathlib, but it seems very doable. Just want to check to make sure we're not duplicating any effort before we start.