Theorem Submodule.IsPrimary.ne_top

Modification history

2024-10-28 20:08
Mathlib/RingTheory/IsPrimary.lean
feat(RingTheory): generalize `Ideal.IsPrimary` to submodules (#17073) …
Added Submodule.IsPrimary.ne_topView on Github →