From 48a7a31ec3409cad2f876ed856190170fcb84109 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Sat, 10 Jun 2023 03:13:59 +0000 Subject: [PATCH] add readme --- Readme.md | 3 +++ comm_alg/grant.lean | 6 ++++++ 2 files changed, 9 insertions(+) create mode 100644 Readme.md create mode 100644 comm_alg/grant.lean 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