From 9a08a5927441d3c59831b1a5e07629b68a51f782 Mon Sep 17 00:00:00 2001
From: GTBarkley <67718465+GTBarkley@users.noreply.github.com>
Date: Sat, 10 Jun 2023 18:40:48 -0400
Subject: [PATCH 1/2] added more references to readme

---
 README.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index d3e6216..058a6e8 100644
--- a/README.md
+++ b/README.md
@@ -9,6 +9,8 @@ Feel free to add, modify, and expand this file. Below are starting points for th
 - Definitions of an ideal, prime ideal, and maximal ideal:
 ```lean
 def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
+class Mathlib.RingTheory.Ideal.Basic.IsPrime (I : Ideal α) : Prop
+class IsMaximal (I : Ideal α) : Prop
 ```
 
 - Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
@@ -31,7 +33,7 @@ Give Examples of each of the above cases for a particular instances of ring
 
 Theorem 0: Hilbert Basis Theorem:
 ```lean
-instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)
+theorem Mathlib.RingTheory.Polynomial.Basic.Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X]
 ```
 
 Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1

From 506fd9b4d6591a7f26143f7ed2355f1e64c07a4b Mon Sep 17 00:00:00 2001
From: GTBarkley <67718465+GTBarkley@users.noreply.github.com>
Date: Sat, 10 Jun 2023 18:53:44 -0400
Subject: [PATCH 2/2] added more references to mathlib to readme

---
 README.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 058a6e8..3c5bba6 100644
--- a/README.md
+++ b/README.md
@@ -18,9 +18,14 @@ class IsMaximal (I : Ideal α) : Prop
 - Definition of a Noetherian and Artinian rings:
 ```lean
 class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
+class Mathlib.RingTheory.Artinian.IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
 ```
+- Definition of a polynomial ring: `Mathlib.RingTheory.Polynomial.Basic`
 
-- Definitions of a local ring and quotient ring
+- Definitions of a local ring and quotient ring: `Mathlib.RingTheory.Ideal.Quotient.?`
+```lean
+class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] extends Nontrivial R : Prop
+```
 
 - Definition of the chain of prime ideals and the length of these chains