Merge pull request #244 from HEPLean/FeynmanDiagrams

feat: Feynman Trees for two complex scalars
HEPLean · Nov 22, 2024 · de89037 · de89037
2 parents 2fecd15 + dc12a3e
commit de89037
Show file tree

Hide file tree

Showing 7 changed files with 696 additions and 55 deletions.
diff --git a/HepLean.lean b/HepLean.lean
@@ -54,8 +54,9 @@ import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4
-import HepLean.FeynmanDiagrams.Instances.TwoRealScalar
 import HepLean.FeynmanDiagrams.Momentum
+import HepLean.FeynmanDiagrams.Wick.Contract
+import HepLean.FeynmanDiagrams.Wick.String
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom

diff --git a/HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean b/HepLean/FeynmanDiagrams/Instances/TwoRealScalar.lean