Theorem Ideal.isPrimary_finsetInf

Modification history

2026-01-21 07:32
Mathlib/RingTheory/Ideal/IsPrimary.lean
feat(RingTheory/IsPrimary): generalize `isPrimary_inf` to submodules (#34061) …
Added Ideal.isPrimary_finsetInfView on Github →