From 4e819719a62247ea1349ded767f63b528f448476 Mon Sep 17 00:00:00 2001
From: Sameer Savkar <sameersavkar@gmail.com>
Date: Thu, 15 Jun 2023 10:26:31 -0700
Subject: [PATCH] Implemented FieldisArtinian lemma

---
 CommAlg/sameer(artinian-rings).lean | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean
index 417cc96..e619c07 100644
--- a/CommAlg/sameer(artinian-rings).lean
+++ b/CommAlg/sameer(artinian-rings).lean
@@ -6,10 +6,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.RingTheory.DedekindDomain.DVR
 
 
-lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : 
-  IsArtinianRing R := by sorry
-
-
+lemma FieldisArtinian (R : Type _) [CommRing R] (h : IsField R) : 
+    IsArtinianRing R := by
+  let inst := h.toField
+  rw [isArtinianRing_iff, isArtinian_iff_wellFounded]
+  apply WellFounded.intro
+  intro I
+  constructor
+  intro J hJI
+  constructor
+  intro K hKJ
+  exfalso
+  rcases Ideal.eq_bot_or_top J with rfl | rfl
+  . exact not_lt_bot hKJ
+  . exact not_top_lt hJI
 
 lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
 (IsArt : IsArtinianRing R) : IsField (R) := by