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

fix: Build

Browse source
This commit is contained in:
jstoobysmith 2024-10-30 05:41:02 +00:00
parent a263069bbc
commit 5e1262eda7
1 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

36
HepLean/Tensors/ComplexLorentz/Units/Basic.lean
View file

@ -92,33 +92,33 @@ scoped[complexLorentzTensor] notation "δR" => rightAltRightUnit
-/
/-- The definitional tensor node relation for `coContrUnit`. -/
lemma tensorNode_coMetric : {δ' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
Color.down Color.up Lorentz.coContrUnit).tensor:= by
lemma tensorNode_coContrUnit : {δ' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
Color.down Color.up Lorentz.coContrUnit).tensor:= by
rfl
/-- The definitional tensor node relation for `contrCoUnit`. -/
lemma tensorNode_contrMetric : {δ | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
Color.up Color.down Lorentz.contrCoUnit).tensor := by
lemma tensorNode_contrCoUnit: {δ | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE complexLorentzTensor
Color.up Color.down Lorentz.contrCoUnit).tensor := by
rfl
/-- The definitional tensor node relation for `altLeftLeftUnit`. -/
lemma tensorNode_altLeftLeftMetric : {δL' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.downL Color.upL Fermion.altLeftLeftUnit).tensor := by
lemma tensorNode_altLeftLeftUnit : {δL' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.downL Color.upL Fermion.altLeftLeftUnit).tensor := by
rfl
/-- The definitional tensor node relation for `leftAltLeftUnit`. -/
lemma tensorNode_leftAltLeftMetric : {δL | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.upL Color.downL Fermion.leftAltLeftUnit).tensor := by
lemma tensorNode_leftAltLeftUnit : {δL | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.upL Color.downL Fermion.leftAltLeftUnit).tensor := by
rfl
/-- The definitional tensor node relation for `altRightRightUnit`. -/
lemma tensorNode_altRightRightMetric : {δR' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.downR Color.upR Fermion.altRightRightUnit).tensor := by
lemma tensorNode_altRightRightUnit: {δR' | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.downR Color.upR Fermion.altRightRightUnit).tensor := by
rfl
/-- The definitional tensor node relation for `rightAltRightUnit`. -/
lemma tensorNode_rightAltRightMetric : {δR | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.upR Color.downR Fermion.rightAltRightUnit).tensor := by
lemma tensorNode_rightAltRightUnit: {δR | μ ν}ᵀ.tensor = (TensorTree.constTwoNodeE
complexLorentzTensor Color.upR Color.downR Fermion.rightAltRightUnit).tensor := by
rfl
/-!
@ -129,37 +129,37 @@ lemma tensorNode_rightAltRightMetric : {δR | μ ν}ᵀ.tensor = (TensorTree.con
/-- The tensor `coContrUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_coContrUnit (g : SL(2,ℂ)) : {g •ₐ δ' | μ ν}ᵀ.tensor = {δ' | μ ν}ᵀ.tensor := by
rw [tensorNode_coMetric, constTwoNodeE]
rw [tensorNode_coContrUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl
/-- The tensor `contrCoUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_contrCoUnit (g : SL(2,ℂ)) : {g •ₐ δ | μ ν}ᵀ.tensor = {δ | μ ν}ᵀ.tensor := by
rw [tensorNode_contrMetric, constTwoNodeE]
rw [tensorNode_contrCoUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl
/-- The tensor `altLeftLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_altLeftLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL' | μ ν}ᵀ.tensor = {δL' | μ ν}ᵀ.tensor := by
rw [tensorNode_altLeftLeftMetric, constTwoNodeE]
rw [tensorNode_altLeftLeftUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl
/-- The tensor `leftAltLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_leftAltLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL | μ ν}ᵀ.tensor = {δL | μ ν}ᵀ.tensor := by
rw [tensorNode_leftAltLeftMetric, constTwoNodeE]
rw [tensorNode_leftAltLeftUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl
/-- The tensor `altRightRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_altRightRightUnit (g : SL(2,ℂ)) : {g •ₐ δR' | μ ν}ᵀ.tensor = {δR' | μ ν}ᵀ.tensor := by
rw [tensorNode_altRightRightMetric, constTwoNodeE]
rw [tensorNode_altRightRightUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl
/-- The tensor `rightAltRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
lemma action_rightAltRightUnit (g : SL(2,ℂ)) : {g •ₐ δR | μ ν}ᵀ.tensor = {δR | μ ν}ᵀ.tensor := by
rw [tensorNode_rightAltRightMetric, constTwoNodeE]
rw [tensorNode_rightAltRightUnit, constTwoNodeE]
rw [← action_constTwoNode _ g]
rfl