diff --git a/Common.lean b/Common.lean
index 39037ec..dc64440 100644
--- a/Common.lean
+++ b/Common.lean
@@ -1,4 +1,3 @@
-import Common.Algebra
 import Common.Finset
 import Common.List
 import Common.Logic
diff --git a/Common/Algebra.lean b/Common/Algebra.lean
deleted file mode 100644
index 46d0ab1..0000000
--- a/Common/Algebra.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Common.Algebra.Classes
\ No newline at end of file
diff --git a/Common/Algebra/Classes.lean b/Common/Algebra/Classes.lean
deleted file mode 100644
index 21ef4c7..0000000
--- a/Common/Algebra/Classes.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Mathlib.Init.Algebra.Classes
-
-/-! # Common.Algebra.Classes
-
-Additional theorems and definitions useful in the context of algebraic classes.
--/
-
-/--
-`IsConnected X lt` means that the binary relation `lt` on `X` is connected, that
-is, either `lt a b` or `lt b a` for any distinct `a` and `b`.
--/
-class IsConnected (α : Type u) (lt : α → α → Prop) : Prop where
-  connected : ∀ a b, a ≠ b → lt a b ∨ lt b a
\ No newline at end of file