diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
index 0326d2e..f02df74 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
@@ -423,10 +423,12 @@ lemma timeOrder_ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     𝓣(ofFieldOpList [φ]) = ofFieldOpList [φ] := by
   rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_ofFieldOpListF_singleton]
 
+/-- The time order of a list `𝓣(φ₀…φₙ)` is equal to
+`𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`-/
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
-      (Finset.filter (fun x =>
-        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
+      (Finset.univ.filter (fun x =>
+        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs))⟩) •
       ofFieldOp (maxTimeField φ φs) * 𝓣(ofFieldOpList (eraseMaxTimeField φ φs)) := by
   rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_eq_maxTimeField_mul_finset]
   rfl
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
index f20cc45..cc93f86 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
@@ -50,12 +50,14 @@ remark naming_convention := "
   This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined
   as a quotient of `FieldOpFreeAlgebra`."
 
-/-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/
+/-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
+  single `𝓕.CrAnFieldOp`. -/
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ
 
-/-- Maps a list creation and annihlation state to the creation and annihlation free-algebra
-  by taking their product. -/
+/-- For a field specification `𝓕`, `ofCrAnListF φs` of `𝓕.FieldOpFreeAlgebra` formed by a
+  list `φs` of `𝓕.CrAnFieldOp`. For example for the list `[φ₁ᶜ, φ₂ᵃ, φ₃ᶜ]` we schematically
+  get `φ₁ᶜφ₂ᵃφ₃ᶜ`. The set of all `ofCrAnListF φs` forms a basis of  `FieldOpFreeAlgebra 𝓕`. -/
 def ofCrAnListF (φs : List 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofCrAnOpF φs).prod
 
 @[simp]
@@ -71,14 +73,16 @@ lemma ofCrAnListF_append (φs φs' : List 𝓕.CrAnFieldOp) :
 lemma ofCrAnListF_singleton (φ : 𝓕.CrAnFieldOp) :
     ofCrAnListF [φ] = ofCrAnOpF φ := by simp [ofCrAnListF]
 
-/-- Maps a state to the sum of creation and annihilation operators in
-  creation and annihilation free-algebra. -/
+/-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
+ `𝓕.FieldOp` by summing over the creation and annihilation components of `𝓕.FieldOp`.
+  For example for `φ₁` an incoming asymptotic field operator we get `φ₁ᶜ`, and for `φ₁` a
+  position field operator we get `φ₁ᶜ + φ₁ᵃ`. -/
 def ofFieldOpF (φ : 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 :=
   ∑ (i : 𝓕.fieldOpToCrAnType φ), ofCrAnOpF ⟨φ, i⟩
 
-/-- Maps a list of states to the creation and annihilation free-algebra by taking
-  the product of their sums of creation and annihlation operators.
-  Roughly `[φ1, φ2]` gets sent to `(φ1ᶜ+ φ1ᵃ) * (φ2ᶜ+ φ2ᵃ)` etc. -/
+/-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
+  list of `𝓕.FieldOp` by summing over the creation and annihilation components.
+  For example, `φ₁` and `φ₂` position states `[φ1, φ2]` gets sent to `(φ1ᶜ+ φ1ᵃ) * (φ2ᶜ+ φ2ᵃ)`. -/
 def ofFieldOpListF (φs : List 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofFieldOpF φs).prod
 
 /-- Coercion from `List 𝓕.FieldOp` to `FieldOpFreeAlgebra 𝓕` through `ofFieldOpListF`. -/
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
index 8f0c9df..ecc22ec 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
@@ -237,7 +237,9 @@ lemma directSum_eq_bosonic_plus_fermionic
     conv_lhs => rw [hx, hy]
     abel
 
-/-- The instance of a graded algebra on `FieldOpFreeAlgebra`. -/
+/-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is graded by `FieldStatistic`.
+  Those `ofCrAnListF φs` for which `φs` has `bosonic` statistics form one part of the grading,
+  whilst those where `φs` has `fermionic` statistics form the other part of the grading. -/
 instance fieldOpFreeAlgebraGrade :
     GradedAlgebra (A := 𝓕.FieldOpFreeAlgebra) statisticSubmodule where
   one_mem := by
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
index 05d8dd6..2cded43 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
@@ -23,18 +23,18 @@ namespace FieldOpFreeAlgebra
 
 open FieldStatistic
 
-/-- The super commutor on the creation and annihlation algebra. For two bosonic operators
-  or a bosonic and fermionic operator this corresponds to the usual commutator
-  whilst for two fermionic operators this corresponds to the anti-commutator. -/
+/-- For a field specification `𝓕`, the super commutator `superCommuteF` is defined as the linear
+  map `𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra` such that
+  `superCommuteF (φ₀ᶜ…φₙᵃ) (φ₀'ᶜ…φₙ'ᶜ)` is equal to
+  `φ₀ᶜ…φₙᵃ * φ₀'ᶜ…φₙ'ᶜ - 𝓢(φ₀ᶜ…φₙᵃ, φ₀'ᶜ…φₙ'ᶜ) φ₀'ᶜ…φₙ'ᶜ * φ₀ᶜ…φₙᵃ`.
+  The notation `[a, b]ₛca` is used for this super commutator.  -/
 noncomputable def superCommuteF : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ]
     𝓕.FieldOpFreeAlgebra :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   Basis.constr ofCrAnListFBasis ℂ fun φs' =>
   ofCrAnListF (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnListF (φs' ++ φs)
 
-/-- The super commutor on the creation and annihlation algebra. For two bosonic operators
-  or a bosonic and fermionic operator this corresponds to the usual commutator
-  whilst for two fermionic operators this corresponds to the anti-commutator. -/
+@[inherit_doc superCommuteF]
 scoped[FieldSpecification.FieldOpFreeAlgebra] notation "[" φs "," φs' "]ₛca" => superCommuteF φs φs'
 
 /-!
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index efa8d8e..3355d54 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -137,6 +137,11 @@ def perturbationTheory : Note where
     .h2 "Field-operator free algebra",
     .name `FieldSpecification.FieldOpFreeAlgebra,
     .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention,
+    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF,
+    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF,
+    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF,
+    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF,
+    .name `FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade,
     .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
     .h2 "Field-operator algebra",
     .name `FieldSpecification.FieldOpAlgebra,
@@ -146,6 +151,7 @@ def perturbationTheory : Note where
     .name `FieldSpecification.crAnTimeOrderSign,
     .name `FieldSpecification.FieldOpFreeAlgebra.timeOrderF,
     .name `FieldSpecification.FieldOpAlgebra.timeOrder,
+    .name `FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset,
     .h1 "Normal ordering",
     .name `FieldSpecification.normalOrderRel,
     .name `FieldSpecification.normalOrderSign,
@@ -169,6 +175,8 @@ def perturbationTheory : Note where
     .h2 "Cardinality",
     .name `WickContraction.card_eq_cardFun,
     .h1 "Time and static contractions",
+    .h1 "Useful results",
+
     .h1 "The three Wick's theorems",
     .name `FieldSpecification.wicks_theorem,
     .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,