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

fix: Missing import

Browse source
This commit is contained in:
jstoobysmith 2024-07-29 08:46:21 -04:00
parent ee7db8aea0
commit 44b26efdaf
2 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean.lean
View file

@ -74,6 +74,7 @@ import HepLean.SpaceTime.LorentzTensor.Basic
import HepLean.SpaceTime.LorentzTensor.Contractions
import HepLean.SpaceTime.LorentzTensor.Fin
import HepLean.SpaceTime.LorentzTensor.LorentzTensorStruct
import HepLean.SpaceTime.LorentzTensor.Notation
import HepLean.SpaceTime.LorentzTensor.RisingLowering
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
import HepLean.SpaceTime.LorentzVector.Basic

2
HepLean/SpaceTime/LorentzTensor/Notation.lean
View file

@ -17,6 +17,8 @@ Some examples:
- `ψᵘ¹ᵘ²φᵤ₁` should correspond to the contraction of the first index of `ψ` and the
only index of `φ`.
- `ψᵘ¹ᵘ² = ψᵘ²ᵘ¹` should define the symmetry of `ψ` under the exchange of its indices.
- `θᵤ₂(ψᵘ¹ᵘ²φᵤ₁) = (θᵤ₂ψᵘ¹ᵘ²)φᵤ₁` should correspond to an associativity properity of
contraction.
It should also be possible to define this generically for any `LorentzTensorStructure`.