Commit 2026-01-21 07:32 491fc7f0

View on Github →

feat(RingTheory/IsPrimary): generalize isPrimary_inf to submodules (#34061) This PR generalizes isPrimary_inf and isPrimary_finset_inf from ideals to submodules.

Estimated changes

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

added theorem Ideal.IsPrimary.inf

added theorem Ideal.isPrimary_finsetInf

deleted theorem Ideal.isPrimary_finset_inf

deleted theorem Ideal.isPrimary_inf

Modified Mathlib/RingTheory/IsPrimary.lean

added theorem Submodule.IsPrimary.mem_or_mem

added theorem Submodule.isPrimary_finsetInf

Modified Mathlib/RingTheory/Lasker.lean