From c4a3211e3f48e1aa4afa33d8e2e9fb8f76e9a37e Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 2 Dec 2024 07:44:44 +0000
Subject: [PATCH] feat: Informal normalOrder_wickMap

---
 HepLean/FeynmanDiagrams/Wick/Algebra.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/HepLean/FeynmanDiagrams/Wick/Algebra.lean b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
index 3782225..4d71f99 100644
--- a/HepLean/FeynmanDiagrams/Wick/Algebra.lean
+++ b/HepLean/FeynmanDiagrams/Wick/Algebra.lean
@@ -115,4 +115,8 @@ informal_definition WickMap where
     the necessary properties for lots of theorems to hold."
   deps :≈ [``WickAlgebra, ``WickMonomial]
 
+informal_lemma normalOrder_wickMap where
+  math :≈ "Any normal ordering maps to zero under a Wick map."
+  deps :≈ [``WickMap, ``WickMonomial.normalOrder]
+
 end Wick