diff --git a/.gitignore b/.gitignore
index e254e15..c666579 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
-.DS_Store
\ No newline at end of file
+.DS_Store
+.cache/
\ No newline at end of file
diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean
new file mode 100644
index 0000000..381680b
--- /dev/null
+++ b/comm_alg/sameer(artinian-rings).lean
@@ -0,0 +1,15 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+
+lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): 
+IsArtinianRing (R⧸I) := by sorry
+
+#check Ideal.IsPrime
+
+lemma IsPrimeMaximal (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime I) : Ideal.IsMaximal I := by sorry
+
+
+-- Use Stacks project proof since it's broken into lemmas