Commit 2025-11-09 13:26 8fe433b7

View on Github →

chore(RingTheory/Ideal): deprecate exists_ideal_liesOver_maximal_of_isIntegral (#31333)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

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

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

deleted theorem Ideal.exists_ideal_liesOver_maximal_of_isIntegral