DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore: Move Modules file for Lorentz vectors

Browse source
This commit is contained in:
jstoobysmith 2024-11-01 12:12:09 +00:00
parent aff9c88f99
commit 9fe30285e0
3 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
View file

@ -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

4
HepLean/SpaceTime/LorentzVector/Modules.lean → HepLean/SpaceTime/LorentzVector/Complex/Modules.lean
View file

@ -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.