Theorem Ideal.IsPrimary.inf

Modification history

2026-01-21 07:32

Mathlib/RingTheory/Ideal/IsPrimary.lean

feat(RingTheory/IsPrimary): generalize `isPrimary_inf` to submodules (#34061) …

Added Ideal.IsPrimary.inf View on Github →