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

Merge pull request #220 from HEPLean/IndexNotation

Browse source 
feat: Add informal lemmas
This commit is contained in:
Joseph Tooby-Smith 2024-10-31 20:16:23 +00:00 • committed by GitHub
commit 16b30667ea
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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' | β β' ⊗