From 1e4da8d51ac538f2d62759ddfb93e0dde4d89783 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 17 Jan 2022 23:42:43 +0000
Subject: [PATCH] refactor(linear_algebra/{tensor,exterior}_algebra): convert
 to a directory (#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.
---
 src/algebra/lie/universal_enveloping.lean                     | 2 +-
 src/linear_algebra/clifford_algebra/basic.lean                | 4 ++--
 .../{exterior_algebra.lean => exterior_algebra/basic.lean}    | 2 +-
 .../{tensor_algebra.lean => tensor_algebra/basic.lean}        | 0
 test/free_algebra.lean                                        | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)
 rename src/linear_algebra/{exterior_algebra.lean => exterior_algebra/basic.lean} (99%)
 rename src/linear_algebra/{tensor_algebra.lean => tensor_algebra/basic.lean} (100%)

diff --git a/src/algebra/lie/universal_enveloping.lean b/src/algebra/lie/universal_enveloping.lean
index 9913e91fe3383..c8bed4612a51d 100644
--- 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
index b40cf5bfc1adb..5e6a00f8c1f2c 100644
--- 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 b/src/linear_algebra/exterior_algebra/basic.lean
similarity index 99%
rename from src/linear_algebra/exterior_algebra.lean
rename to src/linear_algebra/exterior_algebra/basic.lean
index 5ac90548dd8de..649695e8e36e9 100644
--- a/src/linear_algebra/exterior_algebra.lean
+++ b/src/linear_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 b/src/linear_algebra/tensor_algebra/basic.lean
similarity index 100%
rename from src/linear_algebra/tensor_algebra.lean
rename to src/linear_algebra/tensor_algebra/basic.lean
diff --git a/test/free_algebra.lean b/test/free_algebra.lean
index 9ede4d9154842..4e3b18edf7702 100644
--- 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
 
 /-!