refactor: Move around results

HEPLean · Feb 20, 2025 · 5e27e20 · 5e27e20
1 parent 73a3112
commit 5e27e20
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 15 deletions.
diff --git a/PhysLean.lean b/PhysLean.lean
@@ -180,7 +180,7 @@ import PhysLean.PerturbationTheory.WickContraction.TimeCond
 import PhysLean.PerturbationTheory.WickContraction.TimeContract
 import PhysLean.PerturbationTheory.WickContraction.Uncontracted
 import PhysLean.PerturbationTheory.WickContraction.UncontractedList
-import PhysLean.QuantumMechanics.HarmonicOscillator
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator
 import PhysLean.SpaceTime.Basic
 import PhysLean.SpaceTime.CliffordAlgebra
 import PhysLean.StandardModel.Basic

diff --git a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean
@@ -1,13 +1,5 @@
 import Mathlib.Analysis.Calculus.Deriv.Polynomial
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.SpecialFunctions.Exp
-import Mathlib.Analysis.SpecialFunctions.ExpDeriv
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.SpecialFunctions.ExpDeriv
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
-import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
 /-!
 
 # Physicists Hermite Polynomial

diff --git a/.../QuantumMechanics/HarmonicOscillator.lean → ...nics/OneDimension/HarmonicOscillator.lean b/.../QuantumMechanics/HarmonicOscillator.lean → ...nics/OneDimension/HarmonicOscillator.lean
@@ -3,12 +3,6 @@ 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 Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.SpecialFunctions.ExpDeriv
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
-import Mathlib.Analysis.SpecialFunctions.Integrals
-import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
-import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
 import PhysLean.Mathematics.SpecialFunctions.PhyscisistsHermite
 /-!