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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2025-02-10 11:05:03 +00:00
parent b4333f038a
commit 6519b9be36
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
View file

@ -230,7 +230,8 @@ The proof of this result ultimately goes as follows
- `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
(considered as a list with one element) with
`ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`.
- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to rearrange terms.
- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to rearrange
terms.
- Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
-/
lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)