diff --git a/CommAlg.lean b/CommAlg.lean
index e99d3a6..cef13f8 100644
--- a/CommAlg.lean
+++ b/CommAlg.lean
@@ -1 +1,4 @@
-def hello := "world"
\ No newline at end of file
+import Mathlib.Tactic
+def hello := "world"
+
+-- Thank Grant for setting this up.
\ No newline at end of file
diff --git a/README.md b/README.md
index 3c5bba6..8ffbe34 100644
--- a/README.md
+++ b/README.md
@@ -31,6 +31,8 @@ class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] ext
 
 - Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim`
 
+- Krull dimension of a module
+
 - Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height`
 
 
@@ -47,4 +49,6 @@ Theorem 2: If A is a nonzero noetherian ring, then dim A[t] = dim A + 1
 
 Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A
 
+Lemma 0: A ring is artinian iff it is noetherian of dimension 0.
+
 Definition of a graded module