Commit 2026-09-07 13:23 795fd416

View on Github →

chore(RingTheory/Ideal/GoingUp): use Ideal.under (#43414) This PR refactors RingTheory/Ideal/GoingUp.lean to use Ideal.under.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

Modified Mathlib/NumberTheory/NumberField/ExistsRamified.lean

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

deleted theorem Ideal.IsIntegral.comap_lt_comap

deleted theorem Ideal.IsIntegral.comap_ne_bot

deleted theorem Ideal.IsIntegral.eq_bot_of_comap_eq_bot

added theorem Ideal.IsIntegral.eq_bot_of_under_eq_bot

deleted theorem Ideal.IsIntegral.isMaximal_of_isMaximal_comap

added theorem Ideal.IsIntegral.isMaximal_of_isMaximal_under

added theorem Ideal.IsIntegral.under_lt_under

added theorem Ideal.IsIntegral.under_ne_bot

deleted theorem Ideal.comap_lt_comap_of_integral_mem_sdiff

deleted theorem Ideal.comap_ne_bot_of_algebraic_mem

deleted theorem Ideal.comap_ne_bot_of_integral_mem

deleted theorem Ideal.eq_bot_of_comap_eq_bot

added theorem Ideal.eq_bot_of_under_eq_bot

deleted theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'

modified theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal

deleted theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'

modified theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap

added theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_under

added theorem Ideal.isMaximal_under_of_isIntegral_of_isMaximal

added theorem Ideal.under_lt_under_of_integral_mem_sdiff

added theorem Ideal.under_ne_bot_of_algebraic_mem

added theorem Ideal.under_ne_bot_of_integral_mem

Modified Mathlib/RingTheory/Ideal/Int.lean

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean