From 97d219fe2162cf2c1d08aa7d5fa65364a8768f8b Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Sat, 10 Jun 2023 07:27:37 -0700
Subject: [PATCH] added resources file to dump useful links

---
 comm_alg/resources.lean | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 comm_alg/resources.lean

diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean
new file mode 100644
index 0000000..feb671a
--- /dev/null
+++ b/comm_alg/resources.lean
@@ -0,0 +1,40 @@
+/-
+We don't want to reinvent the wheel, but finding
+things in Mathlib can be pretty annoying. This is
+a temporary file intended to be a dumping ground for
+useful lemmas and definitions
+-/
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.Order.Height
+
+variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
+
+--ideals are defined
+#check Ideal R
+
+variable (I : Ideal R)
+
+--as are prime and maximal (they are defined as typeclasses)
+#check (I.IsPrime)
+#check (I.IsMaximal)
+
+--a module being Noetherian is also a class
+#check IsNoetherian M
+#check IsNoetherian I
+
+--a ring is Noetherian if it is Noetherian as a module over itself
+#check IsNoetherianRing R
+
+--ditto for Artinian
+#check IsArtinian M
+#check IsArtinianRing R
+
+--I can't find the theorem that an Artinian ring is noetherian. That could be a good
+--thing to add at some point
+
+
+
+--Here's the main defintion that will be helpful
+#check Set.chainHeight
\ No newline at end of file