Commit 2026-05-13 10:08 21863602
View on Github →refactor(RingTheory): refactor APIs for minimal primes to lessen defeq abuse (#38029)
At the moment, many proofs use the numeric dot notation on arguments of the form (hp : p ∈ I.minimalPrimes) to access the proof of p.IsPrime and the proof that I is contained in p.
In this PR we introduce a predicate Ideal.IsMinimalPrime and provide two API lemmas to get rid of this pattern. In a follow-up PR we refactor the remaining lemmas taking an assumption (hp : p ∈ I.minimalPrimes) and replace it by I.IsMinimalPrime p.