Research proof index

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a i ≤ φs.length, then the following relation holds: 𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ) where s is the exchange sign for φ and the uncontracted fields in φ₀…φᵢ₋₁. The proof of this result ultimately is a consequence of `norma...

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted, then 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ) is equal to the normal ordering of [φsΛ]ᵘᶜ with the 𝓕.FieldOp corresponding to k removed. The proof of this result ultimately is a consequence of definitions.