From 223660606bcd4f57d19b7ad87ba3a98a3bc63da6 Mon Sep 17 00:00:00 2001
From: GTBarkley <67718465+GTBarkley@users.noreply.github.com>
Date: Sat, 10 Jun 2023 15:21:22 -0400
Subject: [PATCH] added bullets and the definition of an ideal from mathlib

---
 README.md | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 9fe7965..25599bc 100644
--- a/README.md
+++ b/README.md
@@ -6,19 +6,22 @@ We start the commutative algebra project with a list of important definitions an
 
 Feel free to add, modify, and expand this file. Below are starting points for the project:
 
-Definitions of an ideal, prime ideal, and maximal ideal
+- Definitions of an ideal, prime ideal, and maximal ideal:
+```lean
+def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
+```
 
-Definition of a Spec of a ring
+- Definition of a Spec of a ring
 
-Definition of a Noetherian and Artinian rings
+- Definition of a Noetherian and Artinian rings
 
-Definitions of a local ring and quotient ring
+- Definitions of a local ring and quotient ring
 
-Definition of the chain of prime ideals and the length of these chains
+- Definition of the chain of prime ideals and the length of these chains
 
-Definition of the Krull dimension (supremum of the lengh of chain of prime ideal) 
+- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal) 
 
-Definition of the height of prime ideal (dimension of A_p)
+- Definition of the height of prime ideal (dimension of A_p)
 
 Give Examples of each of the above cases for a particular instances of ring