added Basic.lean so lake stops complaining

arnavdandu · arnavdandu · commit 4f7b77ae3d98 · 2025-02-04T18:03:31.000-08:00
diff --git a/LeanCommAlg/Basic.lean b/LeanCommAlg/Basic.lean
@@ -0,0 +1 @@
+--need this so that the lake build stops complaining

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+--need this so that the lake build stops complaining`