Commit 2026-01-19 08:37 aa9f5b62
View on Github →refactor(RingTheory/Lasker): create structure for primary decomposition (#33782) This PR extracts the conclusion of the Lasker-Noether theorem into a separate predicate, so that (in a follow-up PR), the various properties of the primary decomposition don't have to rewrite the entire three-line predicate each time.