chore(linear_algebra): flatten hierarchy, move algebra/linear_algebra to linear_algebra

johoelzl · johoelzl · commit d010717f089a · 2018-03-10T12:39:38.000+01:00
diff --git a/algebra/linear_algebra/default.lean b/algebra/linear_algebra/default.lean
diff --git a/linear_algebra/basic.lean b/linear_algebra/basic.lean
diff --git a/linear_algebra/default.lean b/linear_algebra/default.lean
@@ -0,0 +1 @@
+import linear_algebra.basic
diff --git a/linear_algebra/dimension.lean b/linear_algebra/dimension.lean
@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Dimension of modules and vector spaces.
 -/
-import algebra.linear_algebra.basic set_theory.cardinal
+import linear_algebra.basic set_theory.cardinal
 noncomputable theory
 
 local attribute [instance] classical.prop_decidable
diff --git a/linear_algebra/linear_map_module.lean b/linear_algebra/linear_map_module.lean
@@ -5,10 +5,10 @@ Authors: Johannes Hölzl, Kenny Lau
 
 Type of linear functions
 -/
-import algebra.linear_algebra.basic
-  algebra.linear_algebra.prod_module
-  algebra.linear_algebra.quotient_module
-  algebra.linear_algebra.subtype_module
+import linear_algebra.basic
+  linear_algebra.prod_module
+  linear_algebra.quotient_module
+  linear_algebra.subtype_module
 noncomputable theory
 local attribute [instance] classical.prop_decidable
 
diff --git a/linear_algebra/multivariate_polynomial.lean b/linear_algebra/multivariate_polynomial.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Multivariate Polynomial
 -/
-import data.finsupp algebra.linear_algebra.basic
+import data.finsupp linear_algebra.basic
 noncomputable theory
 
 open classical set function finsupp lattice
diff --git a/linear_algebra/prod_module.lean b/linear_algebra/prod_module.lean
@@ -6,7 +6,7 @@ Author: Johannes Hölzl
 Semigroup, monoid, group and module structures on product spaces.
 -/
 
-import data.prod algebra.linear_algebra.basic
+import data.prod linear_algebra.basic
 open set function
 
 universes u v w x
diff --git a/linear_algebra/quotient_module.lean b/linear_algebra/quotient_module.lean
@@ -6,7 +6,7 @@ Author: Johannes Hölzl
 Quotient construction on modules
 -/
 
-import algebra.linear_algebra.basic
+import linear_algebra.basic
 
 namespace is_submodule
 
diff --git a/linear_algebra/subtype_module.lean b/linear_algebra/subtype_module.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau
 
 Subtype construction of sub modules.
 -/
-import algebra.linear_algebra.basic
+import linear_algebra.basic
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
