From e3e8354be5a347d4c75b3dd9206a539a790dc5db Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 13 Feb 2025 11:07:26 +0000 Subject: [PATCH] docs: Update documentation --- HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean index 746baa4..f418ae9 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean @@ -66,7 +66,7 @@ lemma staticWickTerm_insert_zero_none (Ļ† : š“•.FieldOp) (Ļ†s : List š“•.Field - `Ļ†sĪ›.staticContract` - `s ā€¢ [anPart Ļ†, ofFieldOp Ļ†s[k]]ā‚›` where `s` is the sign associated with moving `Ļ†` through uncontracted fields in `Ļ†ā‚€ā€¦Ļ†ā‚–ā‚‹ā‚` -- the normal ordering `š“([Ļ†sĪ›]įµ˜į¶œ.erase (uncontractedFieldOpEquiv Ļ†s Ļ†sĪ› k))`. +- the normal ordering of `[Ļ†sĪ›]įµ˜į¶œ` with the field operator `Ļ†s[k]` removed. The proof of this result ultimately relies on - `staticContract_insert_some` to rewrite static contractions.