diff --git a/HepLean.lean b/HepLean.lean index 7873b51..811047a 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -55,8 +55,8 @@ import HepLean.FeynmanDiagrams.Basic import HepLean.FeynmanDiagrams.Instances.ComplexScalar import HepLean.FeynmanDiagrams.Instances.Phi4 import HepLean.FeynmanDiagrams.Momentum +import HepLean.FeynmanDiagrams.Wick.Algebra import HepLean.FeynmanDiagrams.Wick.Contract -import HepLean.FeynmanDiagrams.Wick.Ring import HepLean.FeynmanDiagrams.Wick.String import HepLean.FlavorPhysics.CKMMatrix.Basic import HepLean.FlavorPhysics.CKMMatrix.Invariants diff --git a/HepLean/FeynmanDiagrams/Wick/Ring.lean b/HepLean/FeynmanDiagrams/Wick/Algebra.lean similarity index 96% rename from HepLean/FeynmanDiagrams/Wick/Ring.lean rename to HepLean/FeynmanDiagrams/Wick/Algebra.lean index dccadbb..410edbf 100644 --- a/HepLean/FeynmanDiagrams/Wick/Ring.lean +++ b/HepLean/FeynmanDiagrams/Wick/Algebra.lean @@ -5,7 +5,8 @@ Authors: Joseph Tooby-Smith -/ import HepLean.FeynmanDiagrams.Basic /-! -# Operator ring + +# Operator algebra Currently this file is only for an example of Wick strings, correpsonding to a theory with two complex scalar fields. The concepts will however generalize.