Theorem Submodule.IsPrimary.mem_or_mem

Modification history

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