SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

added WF_interval_of_no_primes

Browse source
This commit is contained in:
GTBarkley 2023-06-16 05:05:39 +00:00
parent 4cd9bdee41
commit c2f3d77323
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
CommAlg/grant2.lean
View file

@ -55,10 +55,14 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
exact Ideal.mul_mem_left _ _ hs2 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 ): (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry 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 protected lemma LocalRing.height_le_one_of_minimal_over_principle
[LocalRing R] {x : R} [LocalRing R] {x : R}
(h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) : (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :