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

refactor: Change bispinor name

Browse source
This commit is contained in:
jstoobysmith 2024-10-25 13:52:06 +00:00
parent e6ef68d7e6
commit e11bf41f4c
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
View file

@ -30,9 +30,9 @@ def contrBispinorUp (p : complexContr) :=
{p | μ ⊗ pauliCo | μ α β}ᵀ.tensor {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor
/-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/ /-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
def bispinorDown (p : complexContr) := def contrBispinorDown (p : complexContr) :=
{Fermion.altRightMetric | β β' ⊗ Fermion.altLeftMetric | α α' ⊗ {Fermion.altRightMetric | β β' ⊗ Fermion.altLeftMetric | α α' ⊗
(complexContr.bispinorUp p) | α β}ᵀ.tensor (contrBispinorUp p) | α β}ᵀ.tensor
end complexLorentzTensor end complexLorentzTensor
end end