Theorem Ideal.isPrimary_of_isMaximal_radical

Modification history

2026-01-10 21:14
Mathlib/RingTheory/Ideal/IsPrimary.lean
refactor: generalize `isPrimary_of_isMaximal_radical` to `CommSemiring` (#33779) …
Modified Ideal.isPrimary_of_isMaximal_radicalView on Github →
2023-05-18 05:52
Mathlib/RingTheory/JacobsonIdeal.lean
feat port RingTheory.JacobsonIdeal (#4061)
Added Ideal.isPrimary_of_isMaximal_radicalView on Github →