From ea6e12829370d9630a7e65200c8349e9086c05ba Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 3 Feb 2025 12:12:36 +0000 Subject: [PATCH] refactor: move algebra files --- HepLean.lean | 28 +++++++++---------- .../{Algebras => }/FieldOpAlgebra/Basic.lean | 2 +- .../FieldOpAlgebra/NormalOrder.lean | 4 +-- .../FieldOpAlgebra/StaticWickTheorem.lean | 2 +- .../FieldOpAlgebra/SuperCommute.lean | 4 +-- .../FieldOpAlgebra/TimeContraction.lean | 4 +-- .../FieldOpAlgebra/TimeOrder.lean | 4 +-- .../{ => FieldOpAlgebra}/WicksTheorem.lean | 0 .../FieldOpAlgebra/WicksTheoremNormal.lean | 2 +- .../FieldOpFreeAlgebra/Basic.lean | 0 .../FieldOpFreeAlgebra/Grading.lean | 2 +- .../FieldOpFreeAlgebra/NormTimeOrder.lean | 2 +- .../FieldOpFreeAlgebra/NormalOrder.lean | 2 +- .../FieldOpFreeAlgebra/SuperCommute.lean | 4 +-- .../FieldOpFreeAlgebra/TimeOrder.lean | 2 +- .../WickContraction/Basic.lean | 2 +- .../WickContraction/Join.lean | 2 +- .../WickContraction/StaticContract.lean | 2 +- .../WickContraction/SubContraction.lean | 2 +- .../WickContraction/TimeContract.lean | 2 +- README.md | 2 +- 21 files changed, 37 insertions(+), 37 deletions(-) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/Basic.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/NormalOrder.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/StaticWickTheorem.lean (98%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/SuperCommute.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/TimeContraction.lean (97%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/TimeOrder.lean (99%) rename HepLean/PerturbationTheory/{ => FieldOpAlgebra}/WicksTheorem.lean (100%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpAlgebra/WicksTheoremNormal.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/Basic.lean (100%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/Grading.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/NormTimeOrder.lean (94%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/NormalOrder.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/SuperCommute.lean (99%) rename HepLean/PerturbationTheory/{Algebras => }/FieldOpFreeAlgebra/TimeOrder.lean (99%) diff --git a/HepLean.lean b/HepLean.lean index dcd2d01..b6b3c59 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -121,24 +121,25 @@ import HepLean.Meta.Remark.Basic import HepLean.Meta.Remark.Properties import HepLean.Meta.TODO.Basic import HepLean.Meta.TransverseTactics -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.WicksTheoremNormal -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Grading -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.NormTimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.TimeOrder import HepLean.PerturbationTheory.CreateAnnihilate import HepLean.PerturbationTheory.FeynmanDiagrams.Basic import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4 import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum +import HepLean.PerturbationTheory.FieldOpAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Grading +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder import HepLean.PerturbationTheory.FieldSpecification.Basic import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp import HepLean.PerturbationTheory.FieldSpecification.CrAnSection @@ -170,7 +171,6 @@ import HepLean.PerturbationTheory.WickContraction.TimeCond import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.Uncontracted import HepLean.PerturbationTheory.WickContraction.UncontractedList -import HepLean.PerturbationTheory.WicksTheorem import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra import HepLean.StandardModel.Basic diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean index 6c4f2ed..92ac539 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import Mathlib.Algebra.RingQuot import Mathlib.RingTheory.TwoSidedIdeal.Operations /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean index 9eda79a..9b8aab2 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute /-! # Normal Ordering on Field operator algebra diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean similarity index 98% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean index eb4572e..599deef 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.WicksTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem import HepLean.Meta.Remark.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean index 81e06a7..68a1851 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.Basic /-! # SuperCommute on Field operator algebra diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean similarity index 97% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean index f74482e..12d0a42 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 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.Algebras.FieldOpAlgebra.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder /-! # Time contractions diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean index d5407c5..afbf9dd 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute /-! # Time Ordering on Field operator algebra diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean similarity index 100% rename from HepLean/PerturbationTheory/WicksTheorem.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean rename to HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean index ccd787a..d2c6875 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeCond import HepLean.PerturbationTheory.WickContraction.Sign.Join -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem +import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem import HepLean.Meta.Remark.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean similarity index 100% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Basic.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean index 5a8acef..8f0c9df 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/Grading.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign import Mathlib.RingTheory.GradedAlgebra.Basic /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean similarity index 94% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean index 8343080..e247baf 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean index 6dea226..f3212ca 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.NormalOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean index e588bb9..05d8dd6 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean @@ -3,8 +3,8 @@ Copyright (c) 2025 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.Algebras.FieldOpFreeAlgebra.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Grading +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Grading /-! # Super Commute diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean similarity index 99% rename from HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean rename to HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean index e729e32..6a5ec8f 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.FieldSpecification.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute +import HepLean.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute import HepLean.PerturbationTheory.Koszul.KoszulSign /-! diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index 1d27072..b6227ff 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.FieldOpAlgebra.NormalOrder +import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder import HepLean.Mathematics.List.InsertIdx /-! diff --git a/HepLean/PerturbationTheory/WickContraction/Join.lean b/HepLean/PerturbationTheory/WickContraction/Join.lean index b474e61..67b8e5f 100644 --- a/HepLean/PerturbationTheory/WickContraction/Join.lean +++ b/HepLean/PerturbationTheory/WickContraction/Join.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction import HepLean.PerturbationTheory.WickContraction.SubContraction import HepLean.PerturbationTheory.WickContraction.Singleton diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean index 49c368e..e16a083 100644 --- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Sign.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Time contractions diff --git a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean index 0f9d75f..6378c7e 100644 --- a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean +++ b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.StaticContract -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Sub contractions diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index c1d588c..65632aa 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.WickContraction.Sign.Basic -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction /-! # Time contractions diff --git a/README.md b/README.md index e65e975..fa9f716 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ __BSM physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/BeyondThe __Flavor physics [🗂️](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html):__ Properties of the CKM matrix. -__Perturbation Theory [🗂️](https://heplean.github.io/HepLean/docs/HepLean/PerturbationTheory/WicksTheorem.html):__ Time-dependent version of Wick's theorem for both fermions and bosons. +__Perturbation Theory [🗂️](https://heplean.github.io/HepLean/docs/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.html):__ Time-dependent version of Wick's theorem for both fermions and bosons. ## Associated media and publications - [📄](https://arxiv.org/abs/2405.08863) Joseph Tooby-Smith,