Commit 2026-02-01 08:04 1ab12cde

View on Github →

refactor(RingTheory/Lasker): generalize from Ideal to Submodule (#34135) This PR generalizes the Lasker-Noether theorem from ideals to submodules.

Estimated changes

Modified Mathlib/RingTheory/Lasker.lean

deleted theorem Ideal.IsLasker.exists_isMinimalPrimaryDecomposition

deleted structure Ideal.IsMinimalPrimaryDecomposition

deleted theorem Ideal.decomposition_erase_inf

deleted theorem Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

deleted theorem Ideal.isLasker

deleted theorem Ideal.isPrimary_decomposition_pairwise_ne_radical

modified theorem InfIrred.isPrimary

added theorem Submodule.IsLasker.exists_isMinimalPrimaryDecomposition

added structure Submodule.IsMinimalPrimaryDecomposition

added theorem Submodule.decomposition_erase_inf

added theorem Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

added theorem Submodule.isLasker

added theorem Submodule.isPrimary_decomposition_pairwise_ne_radical

Modified docs/1000.yaml