diff --git a/HepLean.lean b/HepLean.lean
index a821102..ea534f2 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -103,6 +103,7 @@ import HepLean.Mathematics.Fin
 import HepLean.Mathematics.LinearMaps
 import HepLean.Mathematics.PiTensorProduct
 import HepLean.Mathematics.SO3.Basic
+import HepLean.Mathematics.SuperAlgebra.Basic
 import HepLean.Meta.AllFilePaths
 import HepLean.Meta.Basic
 import HepLean.Meta.Informal
diff --git a/HepLean/Mathematics/SuperAlgebra/Basic.lean b/HepLean/Mathematics/SuperAlgebra/Basic.lean
new file mode 100644
index 0000000..9496d87
--- /dev/null
+++ b/HepLean/Mathematics/SuperAlgebra/Basic.lean
@@ -0,0 +1,23 @@
+/-
+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 Mathlib.RingTheory.GradedAlgebra.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Super Algebras
+
+A super algebra is a special type of graded algebra.
+
+It is used in physics to model the commutator of fermionic operators among themselves,
+aswell as among bosonic operators.
+
+-/
+
+informal_definition SuperAlgebra where
+  math :≈ "A super algebra is a graded algebra A with a ℤ₂ grading."
+  physics :≈ "A super algebra is used to model the commutator of fermionic operators among
+    themselves, aswell as among bosonic operators."
+  ref :≈ "https://en.wikipedia.org/wiki/Superalgebra"
diff --git a/HepLean/PerturbationTheory/Wick/Algebra.lean b/HepLean/PerturbationTheory/Wick/Algebra.lean
index b5b0a1c..4d1fbe7 100644
--- a/HepLean/PerturbationTheory/Wick/Algebra.lean
+++ b/HepLean/PerturbationTheory/Wick/Algebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Wick.Species
+import HepLean.Mathematics.SuperAlgebra.Basic
 /-!
 
 # Operator algebra
@@ -28,7 +29,7 @@ informal_definition WickAlgebra where
   math :≈ "
     Modifications of this may be needed.
     A structure with the following data:
-    - A ℤ₂-graded algebra A.
+    - A super algebra A.
     - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.
     - A map `ψc : 𝓔 × SpaceTime → A`.
     - A map `ψd : 𝓔 × SpaceTime → A`.
@@ -47,6 +48,7 @@ informal_definition WickAlgebra where
   physics :≈ "This is defined to be an
     abstraction of the notion of an operator algebra."
   ref :≈ "https://physics.stackexchange.com/questions/24157/"
+  deps :≈ [``SuperAlgebra]
 
 informal_definition WickMonomial where
   math :≈ "The type of elements of the Wick algebra which is a product of fields."
diff --git a/HepLean/PerturbationTheory/Wick/Species.lean b/HepLean/PerturbationTheory/Wick/Species.lean
index 0fec956..d9d0733 100644
--- a/HepLean/PerturbationTheory/Wick/Species.lean
+++ b/HepLean/PerturbationTheory/Wick/Species.lean
@@ -22,8 +22,7 @@ namespace Wick
 /-- The basic structure needed to write down Wick contractions for a theory and
   calculate the corresponding Feynman diagrams.
 
-  WARNING: This definition is not yet complete.
-  -/
+  WARNING: This definition is not yet complete. -/
 structure Species where
   /-- The color of Field operators which appear in a theory.
     One may wish to call these `half-edges`, however we restrict this terminology