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

refactor: Fix typos

Browse source
This commit is contained in:
jstoobysmith 2025-02-07 13:19:36 +00:00
parent 33df4b03a9
commit b7ae7dc2ad
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/TimeContract.lean
View file

@ -79,7 +79,7 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
open FieldStatistic
/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
/-- 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` such that `i ≤ k`, with the
condition that `φ` has greater or equal time to `φs[k]`, then
`(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
@ -123,7 +123,7 @@ lemma timeContract_insert_some_of_lt
simp only [exchangeSign_mul_self]
· exact ht
/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
/-- 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` such that `k < i`, with the
condition that `φs[k]` does not have has greater or equal time to `φ`, then
`(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of