From c2f3d773238338bfbd69880d3ad9440cb9134011 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Fri, 16 Jun 2023 05:05:39 +0000 Subject: [PATCH] added WF_interval_of_no_primes --- CommAlg/grant2.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CommAlg/grant2.lean b/CommAlg/grant2.lean index 24edcff..8bf6085 100644 --- a/CommAlg/grant2.lean +++ b/CommAlg/grant2.lean @@ -55,10 +55,14 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where exact Ideal.mul_mem_left _ _ hs2 -theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime] +theorem WF_interval_le_prime [IsNoetherianRing R] (I : Ideal R) (P : Ideal R) [P.IsPrime] (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ): WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry +theorem WF_interval_of_no_primes [IsNoetherianRing R] (I : Ideal R) (J : Ideal R) + (h : ∀ K ∈ (Set.Icc I J), ¬ K.IsPrime) : + WellFounded ((· < ·) : (Set.Icc I J) → (Set.Icc I J) → Prop ) := sorry + protected lemma LocalRing.height_le_one_of_minimal_over_principle [LocalRing R] {x : R} (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :