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

Update NormalOrder.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-23 01:43:55 +01:00
parent 50556354fa
commit bd35e5522d
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
View file

@ -149,7 +149,7 @@ lemma normalOrderSign_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
rw [← normalOrderSign, normalOrderSign_swap_create_annihlate φc φa hφc hφa φs φs']
rw [← mul_assoc, mul_comm _ (FieldStatistic.exchangeSign _ _), mul_assoc]
simp only [FieldStatistic.instCommGroup.eq_1, mul_eq_mul_left_iff]
left
apply Or.inl
conv_rhs => rw [normalOrderSign, Wick.koszulSign, ← normalOrderSign]
simp only [mul_eq_mul_right_iff]
left