Theorem Submodule.isPrimary_finsetInf

Modification history

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