From 7d91d4c2ddaa0934dcb911570cf6953e417a4241 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 13 Feb 2025 12:05:37 +0000
Subject: [PATCH] Update TimeCond.lean

---
 HepLean/PerturbationTheory/WickContraction/TimeCond.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
index ed2a721..2938749 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
@@ -97,7 +97,7 @@ lemma empty_mem {φs : List 𝓕.FieldOp} : empty (n := φs.length).EqTimeOnly :
   simp [empty]
 
 /-- Let `φs` be a list of `𝓕.FieldOp` and `φsΛ` a `WickContraction` of `φs` within
-  which every contraction involves two `𝓕FieldOp`s that have the same time, then
+  which every contraction involves two `𝓕.FieldOp`s that have the same time, then
   `φsΛ.staticContract = φsΛ.timeContract`. -/
 lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
     φsΛ.staticContract = φsΛ.timeContract := by