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

feat: Add vecAsTensor

Browse source
This commit is contained in:
jstoobysmith 2024-07-30 09:29:05 -04:00
parent a438af453d
commit 57d08ffd40
3 changed files with 60 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,7 +34,7 @@ open TensorProduct
variable {R : Type} [CommSemiring R]
/-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/
/-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/
def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
[Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 :=