From 8e7ddca721f0f3eb6eca2eb47ac6434ef9328e06 Mon Sep 17 00:00:00 2001
From: Sameer Savkar <sameersavkar@gmail.com>
Date: Mon, 12 Jun 2023 10:34:51 -0700
Subject: [PATCH] created a new file

---
 .gitignore                           |  3 ++-
 comm_alg/sameer(artinian-rings).lean | 11 +++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 comm_alg/sameer(artinian-rings).lean

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..aae0fd7
--- /dev/null
+++ b/comm_alg/sameer(artinian-rings).lean
@@ -0,0 +1,11 @@
+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 _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry
+
+lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry
+
+-- Use Stacks project proof since it's broken into lemmas