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

Update InsertList.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-23 00:58:22 +01:00
parent 3447a2fc08
commit b078f63ffb
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/PerturbationTheory/WickContraction/InsertList.lean
View file

@ -77,7 +77,7 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· simp [congrLift]
· rw [Fin.lt_def] at h ⊢
simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
omega
/-!
@ -188,7 +188,7 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· simp [congrLift]
· rw [Fin.lt_def] at h ⊢
simp_all only [Nat.succ_eq_add_one, Fin.val_fin_lt, not_lt, finCongr_apply, Fin.coe_cast]
have hi : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j
omega
lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)