✨ Add lean3 version of rubin's wip proof

7 months ago · 6470249db0
commit 6470249db0
4 changed files with 1065 additions and 0 deletions
--- a/README.md
+++ b/README.md
@ -0,0 +1 @@
+# Lean4 port of the proof of Rubin's Theorem
--- a/old/.gitignore
+++ b/old/.gitignore
@ -0,0 +1,3 @@
+*.olean
+/_target
+/leanpkg.path
--- a/old/leanpkg.toml
+++ b/old/leanpkg.toml
@ -0,0 +1,8 @@
+[package]
+name = "rubin_lean3"
+version = "0.1"
+lean_version = "leanprover-community/lean:3.51.1"
+path = "src"
+
+[dependencies]
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4e976107aa81b41822bd5bb2b15c90b1c8a2aa15"}
--- a/old/rubin.lean
+++ b/old/rubin.lean
				`@ -0,0 +1 @@`
				`# Lean4 port of the proof of Rubin's Theorem`