Commit 2024-12-20 10:20 78a1c375

View on Github →

feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal (#19139) Define the set of all prime ideals that lie over an ideal. It is mainly for #19141. This is adapted from the proof in the case of number fields. Thanks to @erdOne for reminding me that something similar was done in flt-regular. I referred to it to make my code a lot simpler.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem coe_primesOverFinset

added theorem one_le_primesOver_ncard

added theorem primesOver_finite

added theorem primesOver_ncard_ne_zero

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.Ideal.map_ne_bot_of_ne_bot

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.exists_ideal_liesOver_maximal_of_isIntegral

added theorem Ideal.ne_bot_of_liesOver_of_ne_bot

added theorem Ideal.under_bot

added theorem Ideal.under_top

added def primesOver

added theorem primesOver_bot

Modified Mathlib/RingTheory/Ideal/Prime.lean

added theorem IsDomain.of_bot_isPrime