Theorem Ideal.isPrimary_iff

Modification history

2024-10-28 20:08

Mathlib/RingTheory/Ideal/IsPrimary.lean

feat(RingTheory): generalize `Ideal.IsPrimary` to submodules (#17073) …

Added Ideal.isPrimary_iff View on Github →