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

refactor: Spelling

Browse source
This commit is contained in:
jstoobysmith 2025-02-07 15:45:50 +00:00
parent f8f1e1757f
commit 4cd71f5ec6
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -230,7 +230,7 @@ The proof of this result ultimetly 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 supercommutors, one for each element of `φsn`.
- The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearange terms.
- The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearrange terms.
- Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof.
-/
lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)