diff --git a/Readme.md b/Readme.md
new file mode 100644
index 0000000..1522392
--- /dev/null
+++ b/Readme.md
@@ -0,0 +1,3 @@
+# Commutative algebra in Lean
+
+Welcome to the repository for definitions and theorems related to Krull dimension and Hilbert polynomials.
\ No newline at end of file
diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
new file mode 100644
index 0000000..80e5d39
--- /dev/null
+++ b/comm_alg/grant.lean
@@ -0,0 +1,6 @@
+import Mathlib.Analysis.Seminorm
+
+def hello : IO Unit := do
+  IO.println "Hello, World!"
+
+#eval hello
\ No newline at end of file