chore: comment out old algebra files

ImperialCollegeLondon · Dec 7, 2024 · 19a0a89 · 19a0a89
1 parent 7af42a2
commit 19a0a89
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/FLT/Junk/Algebra.lean b/FLT/Junk/Algebra.lean
@@ -1,3 +1,4 @@
+#exit
 /-
 Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

diff --git a/FLT/Junk/Algebra2.lean b/FLT/Junk/Algebra2.lean
@@ -1,5 +1,5 @@
-import Mathlib.RingTheory.OreLocalization.Ring
 #exit
+import Mathlib.RingTheory.OreLocalization.Ring
 
 -- extend localization theory to algebras
 -- I should only be doing this in the commutative case