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

Update WicksTheorem.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-23 00:58:26 +01:00
parent a328a9ec39
commit 0cc03c09ad
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/PerturbationTheory/WicksTheorem.lean
View file

@ -173,7 +173,7 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li
congr 1
exact signInsertSome_mul_filter_contracted_of_lt φ φs c i k hk hg
· omega
· have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
· have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_lt]
swap
· exact hlt _