Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-30 09:51 e1c0b0a9

View on Github →

feat(ring_theory/jacobson): Integral extension of Jacobson rings are Jacobson (#4304) Main statement given by is_jacobson_of_is_integral

Estimated changes

Modified src/ring_theory/ideal/over.lean

added theorem ideal.eq_bot_of_comap_eq_bot

added theorem ideal.exists_ideal_over_maximal_of_is_integral

Modified src/ring_theory/jacobson.lean

added theorem ideal.is_jacobson_of_is_integral

Modified src/ring_theory/jacobson_ideal.lean

added theorem ideal.comap_jacobson