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

feat: add coBispinorDown_eq_pauliContrDown_contr

Browse source
This commit is contained in:
jstoobysmith 2024-10-29 10:45:43 +00:00
parent 4756466001
commit 7a50680794
2 changed files with 91 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

49
HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
View file

@ -135,5 +135,54 @@ lemma pauliCoDown_eq_metric_mul_pauliCo :
apply perm_congr _ rfl
decide
set_option maxRecDepth 5000 in
/-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/
lemma pauliContrDown_eq_metric_mul_pauliContr :
{pauliContrDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗
Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ := by
conv =>
lhs
rw [tensorNode_pauliContrDown]
rw [contr_tensor_eq <| contr_prod _ _ _]
rw [perm_contr]
erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _]
rw [perm_tensor_eq <| contr_congr 1 2]
rw [perm_perm]
rw [perm_tensor_eq <| contr_tensor_eq <| contr_congr 1 2]
rw [perm_tensor_eq <| perm_contr _ _]
rw [perm_perm]
rw [perm_tensor_eq <| contr_congr 1 2]
rw [perm_perm]
rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 1 2]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
rw [perm_tensor_eq <| perm_contr _ _]
rw [perm_perm]
rw [perm_tensor_eq <| contr_congr 1 2]
rw [perm_perm]
rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_comm _ _ _ _]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
rw [perm_tensor_eq <| perm_contr _ _]
rw [perm_perm]
rw [perm_tensor_eq <| contr_congr 4 1]
rw [perm_perm]
conv =>
rhs
rw [perm_tensor_eq <| contr_swap _ _]
rw [perm_perm]
erw [perm_tensor_eq <| contr_congr 4 1]
rw [perm_perm]
rw [perm_tensor_eq <| contr_tensor_eq <| contr_swap _ _]
erw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0]
rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
rw [perm_tensor_eq <| perm_contr _ _]
rw [perm_perm]
rw [perm_tensor_eq <| contr_congr 4 1]
rw [perm_perm]
apply perm_congr _ rfl
decide
end complexLorentzTensor