Remove unshackled files

leanprover-community · May 11, 2020 · 55ddbbc · 55ddbbc
1 parent 5c41ca3
commit 55ddbbc
Show file tree

Hide file tree

Showing 8 changed files with 1 addition and 2,876 deletions.
diff --git a/library/init/algebra/default.lean b/library/init/algebra/default.lean
@@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring
-import init.algebra.field init.algebra.ordered_field init.algebra.norm_num init.algebra.functions
+import init.algebra.functions
diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean