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

Update Basic.lean

Browse source
This commit is contained in:
jstoobysmith 2024-11-11 16:59:02 +00:00
parent 1bc878a2d4
commit a00a1020a8
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -193,7 +193,10 @@ def complexLorentzTensor : TensorSpecies where
| Color.downR => by simpa using Fermion.altRightContraction_apply_metric
| Color.up => by simpa using Lorentz.contrCoContraction_apply_metric
| Color.down => by simpa using Lorentz.coContrContraction_apply_metric
namespace complexLorentzTensor
/-- Color for complex Lorentz tensors is decidable. -/
instance : DecidableEq complexLorentzTensor.C := complexLorentzTensor.instDecidableEqColor
lemma basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c))