feat: Add Wick species files
This commit is contained in:
parent
bf4953187e
commit
344d5812fd
3 changed files with 24 additions and 0 deletions
|
@ -101,4 +101,5 @@ informal_lemma timeOrder_pair where
|
|||
``contraction]
|
||||
|
||||
/-! TODO: Need to set up data and structure for vaccum expectation values. -/
|
||||
|
||||
end TwoComplexScalar
|
||||
|
|
22
HepLean/FeynmanDiagrams/Wick/Species.lean
Normal file
22
HepLean/FeynmanDiagrams/Wick/Species.lean
Normal file
|
@ -0,0 +1,22 @@
|
|||
/-
|
||||
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.FeynmanDiagrams.Wick.String
|
||||
/-!
|
||||
|
||||
# Wick Species
|
||||
|
||||
Note: There is very likely a much better name for what we here call a Wick Species.
|
||||
|
||||
A Wick Species is a structure containing the basic information needed to write wick contractions
|
||||
for a theory, and calculate their corresponding Feynman diagrams.
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: There should be some sort of notion of a group action on a Wick Species. -/
|
||||
namespace Wick
|
||||
|
||||
|
||||
end Wick
|
Loading…
Add table
Add a link
Reference in a new issue