Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.radical_eq_jacobson_iff_radical_quotient_eq_ringJacobson
Modification history
2026-10-28 11:47
Mathlib/RingTheory/Jacobson/Ideal.lean
chore(RingTheory/Jacobson): use `Ring.jacobson` throughout the library (#44788) …
Added
Ideal.radical_eq_jacobson_iff_radical_quotient_eq_ringJacobson
View on Github →