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

Update ContrContr.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-13 23:07:53 +01:00
parent 5cfdf5358c
commit af72d87449
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
View file

@ -148,7 +148,7 @@ noncomputable section
/-- The contraction map for the first pair of indices. -/
def contrMapFst := S.contrMap c q.i q.j q.hij
/-- The contractoin map for the second pair of indices. -/
/-- The contraction map for the second pair of indices. -/
def contrMapSnd := S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l q.hkl
/-- The homomorphism one must apply on swapping the order of contractions. -/