Theorem Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'

Modification history

2023-07-04 05:50
Mathlib/RingTheory/Ideal/Over.lean
feat: port RingTheory.Jacobson (#4338)
Deleted Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'View on Github →
2023-05-23 13:58
Mathlib/RingTheory/Ideal/Over.lean
feat: port RingTheory.Ideal.Over (#4270)
Added Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'View on Github →