refactor(linear_algebra/{tensor,exterior}_algebra): convert to a dire…

…ctory (#11513) These files can be quite slow, so it's useful to be able to add new definitions and lemmas in standalone files, rather than in the same file. There are a number of open PRs of mine that make this move as part of a new feature, so let's just move them pre-emptively.
leanprover-community · Jan 17, 2022 · 1e4da8d · 1e4da8d
1 parent 5b36c86
commit 1e4da8d
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git a/src/algebra/lie/universal_enveloping.lean b/src/algebra/lie/universal_enveloping.lean
@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import algebra.lie.of_associative
 import algebra.ring_quot
-import linear_algebra.tensor_algebra
+import linear_algebra.tensor_algebra.basic
 
 /-!
 # Universal enveloping algebra

diff --git a/src/linear_algebra/clifford_algebra/basic.lean b/src/linear_algebra/clifford_algebra/basic.lean
@@ -5,8 +5,8 @@ Authors: Eric Wieser, Utensil Song
 -/
 
 import algebra.ring_quot
-import linear_algebra.tensor_algebra
-import linear_algebra.exterior_algebra
+import linear_algebra.tensor_algebra.basic
+import linear_algebra.exterior_algebra.basic
 import linear_algebra.quadratic_form.basic
 
 /-!

diff --git a/src/linear_algebra/exterior_algebra.lean → ...inear_algebra/exterior_algebra/basic.lean b/src/linear_algebra/exterior_algebra.lean → ...inear_algebra/exterior_algebra/basic.lean
@@ -5,7 +5,7 @@ Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 -/
 
 import algebra.ring_quot
-import linear_algebra.tensor_algebra
+import linear_algebra.tensor_algebra.basic
 import linear_algebra.alternating
 import group_theory.perm.sign
 

diff --git a/src/linear_algebra/tensor_algebra.lean → src/linear_algebra/tensor_algebra/basic.lean b/src/linear_algebra/tensor_algebra.lean → src/linear_algebra/tensor_algebra/basic.lean
diff --git a/test/free_algebra.lean b/test/free_algebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 
-import linear_algebra.exterior_algebra
+import linear_algebra.exterior_algebra.basic
 import linear_algebra.clifford_algebra
 
 /-!