PhysLean.lean

import PhysLean.ClassicalMechanics.Basic
import PhysLean.ClassicalMechanics.DampedHarmonicOscillator.Basic
import PhysLean.ClassicalMechanics.EulerLagrange
import PhysLean.ClassicalMechanics.HamiltonsEquations
import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
import PhysLean.ClassicalMechanics.Mass.MassUnit
import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum
import PhysLean.ClassicalMechanics.RigidBody.Basic
import PhysLean.ClassicalMechanics.RigidBody.SolidSphere
import PhysLean.ClassicalMechanics.Scattering.RigidSphere
import PhysLean.ClassicalMechanics.Vibrations.LinearTriatomic
import PhysLean.ClassicalMechanics.WaveEquation.Basic
import PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
import PhysLean.CondensedMatter.Basic
import PhysLean.CondensedMatter.TightBindingChain.Basic
import PhysLean.Cosmology.Basic
import PhysLean.Cosmology.FLRW.Basic
import PhysLean.Electromagnetism.Basic
import PhysLean.Electromagnetism.Charge.ChargeUnit
import PhysLean.Electromagnetism.Current.CircularCoil
import PhysLean.Electromagnetism.Current.InfiniteWire
import PhysLean.Electromagnetism.Dynamics.Basic
import PhysLean.Electromagnetism.Dynamics.CurrentDensity
import PhysLean.Electromagnetism.Dynamics.Hamiltonian
import PhysLean.Electromagnetism.Dynamics.IsExtrema
import PhysLean.Electromagnetism.Dynamics.KineticTerm
import PhysLean.Electromagnetism.Dynamics.Lagrangian
import PhysLean.Electromagnetism.Kinematics.Boosts
import PhysLean.Electromagnetism.Kinematics.EMPotential
import PhysLean.Electromagnetism.Kinematics.ElectricField
import PhysLean.Electromagnetism.Kinematics.FieldStrength
import PhysLean.Electromagnetism.Kinematics.MagneticField
import PhysLean.Electromagnetism.Kinematics.ScalarPotential
import PhysLean.Electromagnetism.Kinematics.VectorPotential
import PhysLean.Electromagnetism.PointParticle.OneDimension
import PhysLean.Electromagnetism.PointParticle.ThreeDimension
import PhysLean.Electromagnetism.Vacuum.Constant
import PhysLean.Electromagnetism.Vacuum.HarmonicWave
import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
import PhysLean.Mathematics.Calculus.AdjFDeriv
import PhysLean.Mathematics.Calculus.Divergence
import PhysLean.Mathematics.DataStructures.FourTree.Basic
import PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
import PhysLean.Mathematics.DataStructures.Matrix.LieTrace
import PhysLean.Mathematics.Distribution.Basic
import PhysLean.Mathematics.Distribution.PowMul
import PhysLean.Mathematics.FDerivCurry
import PhysLean.Mathematics.Fin
import PhysLean.Mathematics.Fin.Involutions
import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
import PhysLean.Mathematics.InnerProductSpace.Adjoint
import PhysLean.Mathematics.InnerProductSpace.Basic
import PhysLean.Mathematics.InnerProductSpace.Calculus
import PhysLean.Mathematics.LinearMaps
import PhysLean.Mathematics.List
import PhysLean.Mathematics.List.InsertIdx
import PhysLean.Mathematics.List.InsertionSort
import PhysLean.Mathematics.PiTensorProduct
import PhysLean.Mathematics.RatComplexNum
import PhysLean.Mathematics.SO3.Basic
import PhysLean.Mathematics.SchurTriangulation
import PhysLean.Mathematics.SpecialFunctions.PhysHermite
import PhysLean.Mathematics.Trigonometry.Tanh
import PhysLean.Mathematics.VariationalCalculus.Basic
import PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
import PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
import PhysLean.Meta.AllFilePaths
import PhysLean.Meta.Basic
import PhysLean.Meta.Informal.Basic
import PhysLean.Meta.Informal.Post
import PhysLean.Meta.Informal.SemiFormal
import PhysLean.Meta.Linters.Sorry
import PhysLean.Meta.Notes.Basic
import PhysLean.Meta.Notes.HTMLNote
import PhysLean.Meta.Notes.NoteFile
import PhysLean.Meta.Notes.ToHTML
import PhysLean.Meta.Remark.Basic
import PhysLean.Meta.Remark.Properties
import PhysLean.Meta.Sorry
import PhysLean.Meta.TODO.Basic
import PhysLean.Meta.TransverseTactics
import PhysLean.Optics.Basic
import PhysLean.Optics.Polarization.Basic
import PhysLean.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
import PhysLean.Particles.BeyondTheStandardModel.PatiSalam.Basic
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
import PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Potential
import PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
import PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
import PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
import PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations
import PhysLean.Particles.FlavorPhysics.CKMMatrix.Rows
import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
import PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
import PhysLean.Particles.NeutrinoPhysics.Basic
import PhysLean.Particles.StandardModel.AnomalyCancellation.Basic
import PhysLean.Particles.StandardModel.AnomalyCancellation.FamilyMaps
import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
import PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
import PhysLean.Particles.StandardModel.AnomalyCancellation.Permutations
import PhysLean.Particles.StandardModel.Basic
import PhysLean.Particles.StandardModel.HiggsBoson.Basic
import PhysLean.Particles.StandardModel.HiggsBoson.Potential
import PhysLean.Particles.StandardModel.Representations
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
import PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Map
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfPotentialTerm
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
import PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
import PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
import PhysLean.Particles.SuperSymmetry.SU5.Potential
import PhysLean.QFT.AnomalyCancellation.Basic
import PhysLean.QFT.AnomalyCancellation.GroupActions
import PhysLean.QFT.PerturbationTheory.CreateAnnihilate
import PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Basic
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
import PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
import PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic
import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
import PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnSection
import PhysLean.QFT.PerturbationTheory.FieldSpecification.Filters
import PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder
import PhysLean.QFT.PerturbationTheory.FieldSpecification.TimeOrder
import PhysLean.QFT.PerturbationTheory.FieldStatistics.Basic
import PhysLean.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
import PhysLean.QFT.PerturbationTheory.FieldStatistics.OfFinset
import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSign
import PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert
import PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic
import PhysLean.QFT.PerturbationTheory.WickAlgebra.Grading
import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
import PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
import PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
import PhysLean.QFT.PerturbationTheory.WickAlgebra.SuperCommute
import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeContraction
import PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeOrder
import PhysLean.QFT.PerturbationTheory.WickAlgebra.Universality
import PhysLean.QFT.PerturbationTheory.WickAlgebra.WickTerm
import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
import PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
import PhysLean.QFT.PerturbationTheory.WickContraction.Basic
import PhysLean.QFT.PerturbationTheory.WickContraction.Card
import PhysLean.QFT.PerturbationTheory.WickContraction.Erase
import PhysLean.QFT.PerturbationTheory.WickContraction.ExtractEquiv
import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContract
import PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
import PhysLean.QFT.PerturbationTheory.WickContraction.Involutions
import PhysLean.QFT.PerturbationTheory.WickContraction.IsFull
import PhysLean.QFT.PerturbationTheory.WickContraction.Join
import PhysLean.QFT.PerturbationTheory.WickContraction.Perm
import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Basic
import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
import PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Join
import PhysLean.QFT.PerturbationTheory.WickContraction.Singleton
import PhysLean.QFT.PerturbationTheory.WickContraction.StaticContract
import PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction
import PhysLean.QFT.PerturbationTheory.WickContraction.TimeCond
import PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract
import PhysLean.QFT.PerturbationTheory.WickContraction.Uncontracted
import PhysLean.QFT.PerturbationTheory.WickContraction.UncontractedList
import PhysLean.QFT.QED.AnomalyCancellation.Basic
import PhysLean.QFT.QED.AnomalyCancellation.BasisLinear
import PhysLean.QFT.QED.AnomalyCancellation.ConstAbs
import PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear
import PhysLean.QFT.QED.AnomalyCancellation.Even.LineInCubic
import PhysLean.QFT.QED.AnomalyCancellation.Even.Parameterization
import PhysLean.QFT.QED.AnomalyCancellation.LineInPlaneCond
import PhysLean.QFT.QED.AnomalyCancellation.LowDim.One
import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Three
import PhysLean.QFT.QED.AnomalyCancellation.LowDim.Two
import PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear
import PhysLean.QFT.QED.AnomalyCancellation.Odd.LineInCubic
import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
import PhysLean.QFT.QED.AnomalyCancellation.Permutations
import PhysLean.QFT.QED.AnomalyCancellation.Sorts
import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
import PhysLean.QuantumMechanics.FiniteTarget.Basic
import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Examples
import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
import PhysLean.QuantumMechanics.OneDimension.Operators.Commutation
import PhysLean.QuantumMechanics.OneDimension.Operators.Momentum
import PhysLean.QuantumMechanics.OneDimension.Operators.Parity
import PhysLean.QuantumMechanics.OneDimension.Operators.Position
import PhysLean.QuantumMechanics.OneDimension.Operators.Unbounded
import PhysLean.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
import PhysLean.QuantumMechanics.PlanckConstant
import PhysLean.Relativity.Bispinors.Basic
import PhysLean.Relativity.CliffordAlgebra
import PhysLean.Relativity.LorentzAlgebra.Basic
import PhysLean.Relativity.LorentzAlgebra.Basis
import PhysLean.Relativity.LorentzAlgebra.ExponentialMap
import PhysLean.Relativity.LorentzGroup.Basic
import PhysLean.Relativity.LorentzGroup.Boosts.Apply
import PhysLean.Relativity.LorentzGroup.Boosts.Basic
import PhysLean.Relativity.LorentzGroup.Boosts.Generalized
import PhysLean.Relativity.LorentzGroup.Orthochronous.Basic
import PhysLean.Relativity.LorentzGroup.Proper
import PhysLean.Relativity.LorentzGroup.Restricted.Basic
import PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation
import PhysLean.Relativity.LorentzGroup.Rotations
import PhysLean.Relativity.LorentzGroup.ToVector
import PhysLean.Relativity.MinkowskiMatrix
import PhysLean.Relativity.PauliMatrices.AsTensor
import PhysLean.Relativity.PauliMatrices.Basic
import PhysLean.Relativity.PauliMatrices.CliffordAlgebra
import PhysLean.Relativity.PauliMatrices.Relations
import PhysLean.Relativity.PauliMatrices.SelfAdjoint
import PhysLean.Relativity.PauliMatrices.ToTensor
import PhysLean.Relativity.SL2C.Basic
import PhysLean.Relativity.SL2C.SelfAdjoint
import PhysLean.Relativity.Special.ProperTime
import PhysLean.Relativity.Special.TwinParadox.Basic
import PhysLean.Relativity.SpeedOfLight
import PhysLean.Relativity.Tensors.Basic
import PhysLean.Relativity.Tensors.Color.Basic
import PhysLean.Relativity.Tensors.Color.Discrete
import PhysLean.Relativity.Tensors.Color.Lift
import PhysLean.Relativity.Tensors.ComplexTensor.Basic
import PhysLean.Relativity.Tensors.ComplexTensor.Lemmas
import PhysLean.Relativity.Tensors.ComplexTensor.Matrix.Pre
import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Basic
import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
import PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
import PhysLean.Relativity.Tensors.ComplexTensor.OfRat
import PhysLean.Relativity.Tensors.ComplexTensor.Units.Basic
import PhysLean.Relativity.Tensors.ComplexTensor.Units.Pre
import PhysLean.Relativity.Tensors.ComplexTensor.Units.Symm
import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
import PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Basic
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Contraction
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Modules
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Two
import PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Unit
import PhysLean.Relativity.Tensors.Constructors
import PhysLean.Relativity.Tensors.Contraction.Basic
import PhysLean.Relativity.Tensors.Contraction.Basis
import PhysLean.Relativity.Tensors.Contraction.Products
import PhysLean.Relativity.Tensors.Contraction.Pure
import PhysLean.Relativity.Tensors.Dual
import PhysLean.Relativity.Tensors.Elab
import PhysLean.Relativity.Tensors.Evaluation
import PhysLean.Relativity.Tensors.MetricTensor
import PhysLean.Relativity.Tensors.OfInt
import PhysLean.Relativity.Tensors.Product
import PhysLean.Relativity.Tensors.RealTensor.Basic
import PhysLean.Relativity.Tensors.RealTensor.CoVector.Basic
import PhysLean.Relativity.Tensors.RealTensor.Derivative
import PhysLean.Relativity.Tensors.RealTensor.Matrix.Pre
import PhysLean.Relativity.Tensors.RealTensor.Metrics.Basic
import PhysLean.Relativity.Tensors.RealTensor.Metrics.Pre
import PhysLean.Relativity.Tensors.RealTensor.ToComplex
import PhysLean.Relativity.Tensors.RealTensor.Units.Pre
import PhysLean.Relativity.Tensors.RealTensor.Vector.Basic
import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.Basic
import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
import PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
import PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic
import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
import PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Modules
import PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic
import PhysLean.Relativity.Tensors.TensorSpecies.Basic
import PhysLean.Relativity.Tensors.Tensorial
import PhysLean.Relativity.Tensors.UnitTensor
import PhysLean.SpaceAndTime.Space.Basic
import PhysLean.SpaceAndTime.Space.ConstantSliceDist
import PhysLean.SpaceAndTime.Space.CrossProduct
import PhysLean.SpaceAndTime.Space.Derivatives.Basic
import PhysLean.SpaceAndTime.Space.Derivatives.Curl
import PhysLean.SpaceAndTime.Space.Derivatives.Div
import PhysLean.SpaceAndTime.Space.Derivatives.Grad
import PhysLean.SpaceAndTime.Space.Derivatives.Laplacian
import PhysLean.SpaceAndTime.Space.DistConst
import PhysLean.SpaceAndTime.Space.DistOfFunction
import PhysLean.SpaceAndTime.Space.IsDistBounded
import PhysLean.SpaceAndTime.Space.LengthUnit
import PhysLean.SpaceAndTime.Space.Norm
import PhysLean.SpaceAndTime.Space.RadialAngularMeasure
import PhysLean.SpaceAndTime.Space.Slice
import PhysLean.SpaceAndTime.Space.Translations
import PhysLean.SpaceAndTime.SpaceTime.Basic
import PhysLean.SpaceAndTime.SpaceTime.Boosts
import PhysLean.SpaceAndTime.SpaceTime.Derivatives
import PhysLean.SpaceAndTime.SpaceTime.LorentzAction
import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
import PhysLean.SpaceAndTime.Time.Basic
import PhysLean.SpaceAndTime.Time.Derivatives
import PhysLean.SpaceAndTime.Time.TimeMan
import PhysLean.SpaceAndTime.Time.TimeTransMan
import PhysLean.SpaceAndTime.Time.TimeUnit
import PhysLean.SpaceAndTime.TimeAndSpace.Basic
import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
import PhysLean.StatisticalMechanics.BoltzmannConstant
import PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
import PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
import PhysLean.StatisticalMechanics.CanonicalEnsemble.Lemmas
import PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState
import PhysLean.StringTheory.Basic
import PhysLean.StringTheory.FTheory.SU5.Basic
import PhysLean.StringTheory.FTheory.SU5.Charges.AnomalyFree
import PhysLean.StringTheory.FTheory.SU5.Charges.OfRationalSection
import PhysLean.StringTheory.FTheory.SU5.Charges.Viable
import PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic
import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
import PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
import PhysLean.StringTheory.FTheory.SU5.Quanta.Basic
import PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
import PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
import PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
import PhysLean.Thermodynamics.Basic
import PhysLean.Thermodynamics.IdealGas.Basic
import PhysLean.Thermodynamics.Temperature.Basic
import PhysLean.Thermodynamics.Temperature.TemperatureUnits
import PhysLean.Units.Basic
import PhysLean.Units.Dimension
import PhysLean.Units.Examples
import PhysLean.Units.FDeriv
import PhysLean.Units.Integral
import PhysLean.Units.UnitDependent
import PhysLean.Units.WithDim.Area
import PhysLean.Units.WithDim.Basic
import PhysLean.Units.WithDim.Energy
import PhysLean.Units.WithDim.Mass
import PhysLean.Units.WithDim.Momentum
import PhysLean.Units.WithDim.Pressure
import PhysLean.Units.WithDim.Speed
import PhysLean.Units.WithDim.Velocity