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

docs: Colors of Lorentz tensors

Browse source
This commit is contained in:
jstoobysmith 2024-11-26 12:35:52 +00:00
parent 08a3607c3a
commit 88b2d28431
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/Lorentz/ComplexTensor/Basic.lean
View file

@ -30,11 +30,17 @@ namespace complexLorentzTensor
/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
inductive Color
/-- The color associated with Left handed fermions. -/
| upL : Color
/-- The color associated with alt-Left handed fermions. -/
| downL : Color
/-- The color associated with Right handed fermions. -/
| upR : Color
/-- The color associated with alt-Right handed fermions. -/
| downR : Color
/-- The color associated with contravariant Lorentz vectors. -/
| up : Color
/-- The color associated with covariant Lorentz vectors. -/
| down : Color
/-- Color for complex Lorentz tensors is decidable. -/