Commit 2026-05-12 10:45 547e34b5

View on Github →

chore(RingTheory/Ideal/GoingUp): weaken IsIntegralClosure to Algebra.IsIntegral (#39070) Several results in GoingUp.lean assumed IsIntegralClosure when they only used Algebra.IsIntegral.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

deleted theorem Ring.DimensionLEOne.isIntegralClosure

added theorem Ring.DimensionLEOne.of_isIntegral

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

deleted theorem Ideal.IntegralClosure.comap_lt_comap

deleted theorem Ideal.IntegralClosure.comap_ne_bot

deleted theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot

deleted theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap

added theorem Ideal.IsIntegral.comap_lt_comap

added theorem Ideal.IsIntegral.comap_ne_bot

added theorem Ideal.IsIntegral.eq_bot_of_comap_eq_bot

added theorem Ideal.IsIntegral.isMaximal_of_isMaximal_comap

deleted theorem Ideal.IsIntegralClosure.comap_lt_comap

deleted theorem Ideal.IsIntegralClosure.comap_ne_bot

deleted theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot

deleted theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap