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

feat: Informal superCommuator

Browse source
This commit is contained in:
jstoobysmith 2024-12-03 15:26:06 +00:00
parent b57e042f1a
commit fbc3abd83e
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/PerturbationTheory/Wick/Contract.lean
View file

@ -27,7 +27,8 @@ inductive WickContract : {ni : ℕ} → {i : Fin ni → S.𝓯} → {n : ℕ}
(str : WickString i c o final) →
{k : ℕ} → (b1 : Fin k → Fin n) → (b2 : Fin k → Fin n) → Type where
| string {ni : ℕ} {i : Fin ni → S.𝓯} {n : ℕ} {c : Fin n → S.𝓯}
{no : ℕ} {o : Fin no → S.𝓯} {str : WickString i c o final} : WickContract str Fin.elim0 Fin.elim0
{no : ℕ} {o : Fin no → S.𝓯}
{str : WickString i c o final} : WickContract str Fin.elim0 Fin.elim0
| contr {ni : ℕ} {i : Fin ni → S.𝓯} {n : ℕ} {c : Fin n → S.𝓯}
{no : ℕ} {o : Fin no → S.𝓯} {str : WickString i c o final} {k : ℕ}
{b1 : Fin k → Fin n} {b2 : Fin k → Fin n} : (i : Fin n) →