Commit 2026-01-10 21:14 c2ac49c1

View on Github →

refactor: generalize isPrimary_of_isMaximal_radical to CommSemiring (#33779) This PR generalizes isPrimary_of_isMaximal_radical to CommSemiring and moves it earlier to IsPrimary.lean.

Estimated changes