fix: build

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -23,9 +23,6 @@ We will formally define the operator ring, in terms of the fields present in the
 -/
 
 namespace Wick
-open CategoryTheory
-open FeynmanDiagram
-open PreFeynmanRule
 
 informal_definition WickAlgebra where
   math :≈ "

HepLean/PerturbationTheory/Wick/Contract.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Wick.String
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Data.Fintype.Sum
+import Mathlib.Logic.Equiv.Fin
 /-!
 
 # Wick Contract
@@ -18,9 +21,6 @@ theory with two complex scalar fields. The concepts will however generalize.
 -/
 
 namespace TwoComplexScalar
-open CategoryTheory
-open FeynmanDiagram
-open PreFeynmanRule
 
 /-- A Wick contraction for a Wick string is a series of pairs `i` and `j` of indices
   to be contracted, subject to ordering and subject to the condition that they can

HepLean/PerturbationTheory/Wick/String.lean

@@ -3,7 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.Wick.Species
+import HepLean.Meta.Informal
+import Mathlib.Data.Fin.Tuple.Basic
 /-!
 # Wick strings
 
@@ -19,9 +20,6 @@ term in the ring of operators. This has yet to be implemented.
 -/
 
 namespace TwoComplexScalar
-open CategoryTheory
-open FeynmanDiagram
-open PreFeynmanRule
 
 /-- The colors of edges which one can associate with a vertex for a theory
   with two complex scalar fields. -/

HepLean/PerturbationTheory/Wick/Theorem.lean

@@ -13,9 +13,6 @@ Wick's theorem is related to a result in probability theory called Isserlis' the
 -/
 
 namespace Wick
-open CategoryTheory
-open FeynmanDiagram
-open PreFeynmanRule
 
 informal_lemma wicks_theorem where
   math :≈ "Wick's theorem for fields which are not normally ordered."