Commit 2024-10-28 20:08 2d770eb4

View on Github →

feat(RingTheory): generalize Ideal.IsPrimary to submodules (#17073) in preparation of the Lasker-Noether theorem over submodules

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime.lean

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

deleted def Ideal.IsPrimary

modified theorem Ideal.IsPrime.isPrimary

added theorem Ideal.isPrimary_iff

modified theorem Ideal.isPrimary_inf

modified theorem Ideal.isPrime_radical

Created Mathlib/RingTheory/IsPrimary.lean

added theorem Submodule.IsPrimary.ne_top

added theorem Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul

Modified Mathlib/RingTheory/JacobsonIdeal.lean

Modified Mathlib/RingTheory/Lasker.lean