From 9fe30285e07e2cc48781dc303e0446a57dc8f293 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 Nov 2024 12:12:09 +0000
Subject: [PATCH] chore: Move Modules file for Lorentz vectors

---
 HepLean.lean                                               | 2 +-
 HepLean/SpaceTime/LorentzVector/Complex/Basic.lean         | 2 +-
 HepLean/SpaceTime/LorentzVector/{ => Complex}/Modules.lean | 4 +---
 3 files changed, 3 insertions(+), 5 deletions(-)
 rename HepLean/SpaceTime/LorentzVector/{ => Complex}/Modules.lean (98%)

diff --git a/HepLean.lean b/HepLean.lean
index ceefbd3..ad3cb24 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -84,11 +84,11 @@ import HepLean.SpaceTime.LorentzVector.Basic
 import HepLean.SpaceTime.LorentzVector.Complex.Basic
 import HepLean.SpaceTime.LorentzVector.Complex.Contraction
 import HepLean.SpaceTime.LorentzVector.Complex.Metric
+import HepLean.SpaceTime.LorentzVector.Complex.Modules
 import HepLean.SpaceTime.LorentzVector.Complex.Two
 import HepLean.SpaceTime.LorentzVector.Complex.Unit
 import HepLean.SpaceTime.LorentzVector.Covariant
 import HepLean.SpaceTime.LorentzVector.LorentzAction
-import HepLean.SpaceTime.LorentzVector.Modules
 import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.PauliMatrices.AsTensor
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
index aeed668..cbcf7de 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.SpaceTime.LorentzVector.Modules
+import HepLean.SpaceTime.LorentzVector.Complex.Modules
 import HepLean.Meta.Informal
 import Mathlib.RepresentationTheory.Rep
 import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
diff --git a/HepLean/SpaceTime/LorentzVector/Modules.lean b/HepLean/SpaceTime/LorentzVector/Complex/Modules.lean
similarity index 98%
rename from HepLean/SpaceTime/LorentzVector/Modules.lean
rename to HepLean/SpaceTime/LorentzVector/Complex/Modules.lean
index b012d7b..bb818f2 100644
--- a/HepLean/SpaceTime/LorentzVector/Modules.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Modules.lean
@@ -9,9 +9,7 @@ import Mathlib.RepresentationTheory.Rep
 import Mathlib.Logic.Equiv.TransferInstance
 /-!
 
-## Modules associated with Lorentz vectors
-
-These have not yet been fully-implmented.
+## Modules associated with complex Lorentz vectors
 
 We define these modules to prevent casting between different types of Lorentz vectors.