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

clean Lorentz

Browse source
This commit is contained in:
Pietro Monticone 2025-01-14 01:29:44 +01:00
parent ebde396335
commit f896988894
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Lorentz/ComplexTensor/Basic.lean
View file

@ -22,7 +22,7 @@ open MonoidalCategory
namespace complexLorentzTensor
/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
/-- The colors associated with complex representations of SL(2, ℂ) of interest to physics. -/
inductive Color
/-- The color associated with Left handed fermions. -/
| upL : Color

2
HepLean/Lorentz/ComplexTensor/Basis.lean
View file

@ -77,7 +77,7 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
rw [basis_eq_FD]
/-- The `perm` node acting on basis vectors corresponds to a basis vector, as a tensor tree
structue. -/
structure. -/
lemma perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
{c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) :