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

feat: Add informal lemma

Browse source
This commit is contained in:
jstoobysmith 2024-10-31 19:52:07 +00:00
parent bb4456c077
commit aff9c88f99
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -88,6 +88,16 @@ lemma tensorNode_coBispinorDown (p : complexCo) :
-/
informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where
math :≈ "{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ"
proof :≈ "Expand `contrBispinorDown` and use fact that metrics contract to the identity."
deps :≈ [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric]
informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where
math :≈ "{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ"
proof :≈ "Expand `coBispinorDown` and use fact that metrics contract to the identity."
deps :≈ [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric]
lemma contrBispinorDown_expand (p : complexContr) :
{contrBispinorDown p | α β}ᵀ.tensor =
{εL' | α α' ⊗ εR' | β β' ⊗