-
Notifications
You must be signed in to change notification settings - Fork 89
Expand file tree
/
Copy pathPhyslib.lean
More file actions
414 lines (413 loc) · 25.9 KB
/
Physlib.lean
File metadata and controls
414 lines (413 loc) · 25.9 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
module
public import Physlib.ClassicalFieldTheory.Local.Variation
public import Physlib.ClassicalMechanics.Basic
public import Physlib.ClassicalMechanics.DampedHarmonicOscillator.Basic
public import Physlib.ClassicalMechanics.EulerLagrange
public import Physlib.ClassicalMechanics.HamiltonsEquations
public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic
public import Physlib.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
public import Physlib.ClassicalMechanics.HarmonicOscillator.Solution
public import Physlib.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
public import Physlib.ClassicalMechanics.Mass.MassUnit
public import Physlib.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
public import Physlib.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
public import Physlib.ClassicalMechanics.RigidBody.Basic
public import Physlib.ClassicalMechanics.RigidBody.SolidSphere
public import Physlib.ClassicalMechanics.Scattering.RigidSphere
public import Physlib.ClassicalMechanics.Vibrations.LinearTriatomic
public import Physlib.ClassicalMechanics.WaveEquation.Basic
public import Physlib.ClassicalMechanics.WaveEquation.HarmonicWave
public import Physlib.CondensedMatter.Basic
public import Physlib.CondensedMatter.TightBindingChain.Basic
public import Physlib.Cosmology.Basic
public import Physlib.Cosmology.FLRW.Basic
public import Physlib.Electromagnetism.Basic
public import Physlib.Electromagnetism.Charge.ChargeUnit
public import Physlib.Electromagnetism.Current.CircularCoil
public import Physlib.Electromagnetism.Current.InfiniteWire
public import Physlib.Electromagnetism.Dynamics.Basic
public import Physlib.Electromagnetism.Dynamics.CurrentDensity
public import Physlib.Electromagnetism.Dynamics.Hamiltonian
public import Physlib.Electromagnetism.Dynamics.IsExtrema
public import Physlib.Electromagnetism.Dynamics.KineticTerm
public import Physlib.Electromagnetism.Dynamics.Lagrangian
public import Physlib.Electromagnetism.Kinematics.Boosts
public import Physlib.Electromagnetism.Kinematics.EMPotential
public import Physlib.Electromagnetism.Kinematics.ElectricField
public import Physlib.Electromagnetism.Kinematics.FieldStrength
public import Physlib.Electromagnetism.Kinematics.MagneticField
public import Physlib.Electromagnetism.Kinematics.ScalarPotential
public import Physlib.Electromagnetism.Kinematics.VectorPotential
public import Physlib.Electromagnetism.PointParticle.OneDimension
public import Physlib.Electromagnetism.PointParticle.ThreeDimension
public import Physlib.Electromagnetism.ThreeDimension.Basic
public import Physlib.Electromagnetism.ThreeDimension.MaxwellEquations
public import Physlib.Electromagnetism.Vacuum.Constant
public import Physlib.Electromagnetism.Vacuum.HarmonicWave
public import Physlib.Electromagnetism.Vacuum.IsPlaneWave
public import Physlib.Mathematics.Calculus.AdjFDeriv
public import Physlib.Mathematics.Calculus.Divergence
public import Physlib.Mathematics.DataStructures.FourTree.Basic
public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
public import Physlib.Mathematics.Distribution.Basic
public import Physlib.Mathematics.Distribution.PowMul
public import Physlib.Mathematics.FDerivCurry
public import Physlib.Mathematics.Fin
public import Physlib.Mathematics.Fin.Involutions
public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs
public import Physlib.Mathematics.InnerProductSpace.Adjoint
public import Physlib.Mathematics.InnerProductSpace.Basic
public import Physlib.Mathematics.InnerProductSpace.Calculus
public import Physlib.Mathematics.InnerProductSpace.Submodule
public import Physlib.Mathematics.KroneckerDelta
public import Physlib.Mathematics.LinearMaps
public import Physlib.Mathematics.List
public import Physlib.Mathematics.List.InsertIdx
public import Physlib.Mathematics.List.InsertionSort
public import Physlib.Mathematics.PiTensorProduct
public import Physlib.Mathematics.RatComplexNum
public import Physlib.Mathematics.SO3.Basic
public import Physlib.Mathematics.SchurTriangulation
public import Physlib.Mathematics.SpecialFunctions.PhysHermite
public import Physlib.Mathematics.Trigonometry.Tanh
public import Physlib.Mathematics.VariationalCalculus.Basic
public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
public import Physlib.Mathematics.VariationalCalculus.HasVarAdjoint
public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
public import Physlib.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
public import Physlib.Mathematics.VariationalCalculus.IsTestFunction
public import Physlib.Meta.AllFilePaths
public import Physlib.Meta.Basic
public import Physlib.Meta.Informal.Basic
public import Physlib.Meta.Informal.Post
public import Physlib.Meta.Informal.SemiFormal
public import Physlib.Meta.Linters.Sorry
public import Physlib.Meta.Notes.Basic
public import Physlib.Meta.Notes.HTMLNote
public import Physlib.Meta.Notes.NoteFile
public import Physlib.Meta.Notes.ToHTML
public import Physlib.Meta.Remark.Basic
public import Physlib.Meta.Remark.Properties
public import Physlib.Meta.Sorry
public import Physlib.Meta.TODO.Basic
public import Physlib.Meta.TransverseTactics
public import Physlib.Optics.Basic
public import Physlib.Optics.Polarization.Basic
public import Physlib.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
public import Physlib.Particles.BeyondTheStandardModel.PatiSalam.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
public import Physlib.Particles.BeyondTheStandardModel.Spin10.Basic
public import Physlib.Particles.BeyondTheStandardModel.TwoHDM.Basic
public import Physlib.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
public import Physlib.Particles.BeyondTheStandardModel.TwoHDM.Potential
public import Physlib.Particles.FlavorPhysics.CKMMatrix.Basic
public import Physlib.Particles.FlavorPhysics.CKMMatrix.Invariants
public import Physlib.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
public import Physlib.Particles.FlavorPhysics.CKMMatrix.Relations
public import Physlib.Particles.FlavorPhysics.CKMMatrix.Rows
public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
public import Physlib.Particles.NeutrinoPhysics.Basic
public import Physlib.Particles.StandardModel.AnomalyCancellation.Basic
public import Physlib.Particles.StandardModel.AnomalyCancellation.FamilyMaps
public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
public import Physlib.Particles.StandardModel.AnomalyCancellation.Permutations
public import Physlib.Particles.StandardModel.Basic
public import Physlib.Particles.StandardModel.HiggsBoson.Basic
public import Physlib.Particles.StandardModel.HiggsBoson.Potential
public import Physlib.Particles.StandardModel.Representations
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Map
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimalSuperSet
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.Basic
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.FinsetTerms
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.MinimallyAllowsTerm.OfFinset
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfPotentialTerm
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoClosed
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrained
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
public import Physlib.Particles.SuperSymmetry.SU5.FieldLabels
public import Physlib.Particles.SuperSymmetry.SU5.Potential
public import Physlib.QFT.AnomalyCancellation.Basic
public import Physlib.QFT.AnomalyCancellation.GroupActions
public import Physlib.QFT.PerturbationTheory.CreateAnnihilate
public import Physlib.QFT.PerturbationTheory.FeynmanDiagrams.Basic
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
public import Physlib.QFT.PerturbationTheory.FieldSpecification.Basic
public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnSection
public import Physlib.QFT.PerturbationTheory.FieldSpecification.Filters
public import Physlib.QFT.PerturbationTheory.FieldSpecification.NormalOrder
public import Physlib.QFT.PerturbationTheory.FieldSpecification.TimeOrder
public import Physlib.QFT.PerturbationTheory.FieldStatistics.Basic
public import Physlib.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
public import Physlib.QFT.PerturbationTheory.FieldStatistics.OfFinset
public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSign
public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSignInsert
public import Physlib.QFT.PerturbationTheory.WickAlgebra.Basic
public import Physlib.QFT.PerturbationTheory.WickAlgebra.Grading
public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
public import Physlib.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
public import Physlib.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
public import Physlib.QFT.PerturbationTheory.WickAlgebra.SuperCommute
public import Physlib.QFT.PerturbationTheory.WickAlgebra.TimeContraction
public import Physlib.QFT.PerturbationTheory.WickAlgebra.TimeOrder
public import Physlib.QFT.PerturbationTheory.WickAlgebra.Universality
public import Physlib.QFT.PerturbationTheory.WickAlgebra.WickTerm
public import Physlib.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
public import Physlib.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
public import Physlib.QFT.PerturbationTheory.WickContraction.Basic
public import Physlib.QFT.PerturbationTheory.WickContraction.Card
public import Physlib.QFT.PerturbationTheory.WickContraction.Erase
public import Physlib.QFT.PerturbationTheory.WickContraction.ExtractEquiv
public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContract
public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
public import Physlib.QFT.PerturbationTheory.WickContraction.Involutions
public import Physlib.QFT.PerturbationTheory.WickContraction.IsFull
public import Physlib.QFT.PerturbationTheory.WickContraction.Join
public import Physlib.QFT.PerturbationTheory.WickContraction.Perm
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.Basic
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.Join
public import Physlib.QFT.PerturbationTheory.WickContraction.Singleton
public import Physlib.QFT.PerturbationTheory.WickContraction.StaticContract
public import Physlib.QFT.PerturbationTheory.WickContraction.SubContraction
public import Physlib.QFT.PerturbationTheory.WickContraction.TimeCond
public import Physlib.QFT.PerturbationTheory.WickContraction.TimeContract
public import Physlib.QFT.PerturbationTheory.WickContraction.Uncontracted
public import Physlib.QFT.PerturbationTheory.WickContraction.UncontractedList
public import Physlib.QFT.QED.AnomalyCancellation.Basic
public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear
public import Physlib.QFT.QED.AnomalyCancellation.ConstAbs
public import Physlib.QFT.QED.AnomalyCancellation.Even.BasisLinear
public import Physlib.QFT.QED.AnomalyCancellation.Even.LineInCubic
public import Physlib.QFT.QED.AnomalyCancellation.Even.Parameterization
public import Physlib.QFT.QED.AnomalyCancellation.LineInPlaneCond
public import Physlib.QFT.QED.AnomalyCancellation.LowDim.One
public import Physlib.QFT.QED.AnomalyCancellation.LowDim.Three
public import Physlib.QFT.QED.AnomalyCancellation.LowDim.Two
public import Physlib.QFT.QED.AnomalyCancellation.Odd.BasisLinear
public import Physlib.QFT.QED.AnomalyCancellation.Odd.LineInCubic
public import Physlib.QFT.QED.AnomalyCancellation.Odd.Parameterization
public import Physlib.QFT.QED.AnomalyCancellation.Permutations
public import Physlib.QFT.QED.AnomalyCancellation.Sorts
public import Physlib.QFT.QED.AnomalyCancellation.VectorLike
public import Physlib.QuantumMechanics.DDimensions.Hydrogen.Basic
public import Physlib.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector
public import Physlib.QuantumMechanics.DDimensions.Operators.AngularMomentum
public import Physlib.QuantumMechanics.DDimensions.Operators.Commutation
public import Physlib.QuantumMechanics.DDimensions.Operators.Momentum
public import Physlib.QuantumMechanics.DDimensions.Operators.Position
public import Physlib.QuantumMechanics.DDimensions.Operators.Unbounded
public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
public import Physlib.QuantumMechanics.FiniteTarget.Basic
public import Physlib.QuantumMechanics.FiniteTarget.HilbertSpace
public import Physlib.QuantumMechanics.OneDimension.GeneralPotential.Basic
public import Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
public import Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
public import Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
public import Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.Examples
public import Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.Basic
public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
public import Physlib.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
public import Physlib.QuantumMechanics.OneDimension.Operators.Commutation
public import Physlib.QuantumMechanics.OneDimension.Operators.Momentum
public import Physlib.QuantumMechanics.OneDimension.Operators.Parity
public import Physlib.QuantumMechanics.OneDimension.Operators.Position
public import Physlib.QuantumMechanics.OneDimension.Operators.Unbounded
public import Physlib.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
public import Physlib.QuantumMechanics.PlanckConstant
public import Physlib.Relativity.Bispinors.Basic
public import Physlib.Relativity.CliffordAlgebra
public import Physlib.Relativity.LorentzAlgebra.Basic
public import Physlib.Relativity.LorentzAlgebra.Basis
public import Physlib.Relativity.LorentzAlgebra.ExponentialMap
public import Physlib.Relativity.LorentzGroup.Basic
public import Physlib.Relativity.LorentzGroup.Boosts.Apply
public import Physlib.Relativity.LorentzGroup.Boosts.Basic
public import Physlib.Relativity.LorentzGroup.Boosts.Generalized
public import Physlib.Relativity.LorentzGroup.Orthochronous.Basic
public import Physlib.Relativity.LorentzGroup.Proper
public import Physlib.Relativity.LorentzGroup.Restricted.Basic
public import Physlib.Relativity.LorentzGroup.Restricted.FromBoostRotation
public import Physlib.Relativity.LorentzGroup.Rotations
public import Physlib.Relativity.LorentzGroup.ToVector
public import Physlib.Relativity.MinkowskiMatrix
public import Physlib.Relativity.PauliMatrices.AsTensor
public import Physlib.Relativity.PauliMatrices.Basic
public import Physlib.Relativity.PauliMatrices.CliffordAlgebra
public import Physlib.Relativity.PauliMatrices.Relations
public import Physlib.Relativity.PauliMatrices.SelfAdjoint
public import Physlib.Relativity.PauliMatrices.ToTensor
public import Physlib.Relativity.SL2C.Basic
public import Physlib.Relativity.SL2C.SelfAdjoint
public import Physlib.Relativity.Special.ProperTime
public import Physlib.Relativity.Special.TwinParadox.Basic
public import Physlib.Relativity.SpeedOfLight
public import Physlib.Relativity.Tensors.Basic
public import Physlib.Relativity.Tensors.Color.Basic
public import Physlib.Relativity.Tensors.Color.Discrete
public import Physlib.Relativity.Tensors.Color.Lift
public import Physlib.Relativity.Tensors.ComplexTensor.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Lemmas
public import Physlib.Relativity.Tensors.ComplexTensor.Matrix.Pre
public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Pre
public import Physlib.Relativity.Tensors.ComplexTensor.OfRat
public import Physlib.Relativity.Tensors.ComplexTensor.Units.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Units.Pre
public import Physlib.Relativity.Tensors.ComplexTensor.Units.Symm
public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Contraction
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Metric
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Modules
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Two
public import Physlib.Relativity.Tensors.ComplexTensor.Weyl.Unit
public import Physlib.Relativity.Tensors.Constructors
public import Physlib.Relativity.Tensors.Contraction.Basic
public import Physlib.Relativity.Tensors.Contraction.Basis
public import Physlib.Relativity.Tensors.Contraction.Products
public import Physlib.Relativity.Tensors.Contraction.Pure
public import Physlib.Relativity.Tensors.Dual
public import Physlib.Relativity.Tensors.Elab
public import Physlib.Relativity.Tensors.Evaluation
public import Physlib.Relativity.Tensors.MetricTensor
public import Physlib.Relativity.Tensors.OfInt
public import Physlib.Relativity.Tensors.Product
public import Physlib.Relativity.Tensors.RealTensor.Basic
public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic
public import Physlib.Relativity.Tensors.RealTensor.Derivative
public import Physlib.Relativity.Tensors.RealTensor.Matrix.Pre
public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
public import Physlib.Relativity.Tensors.RealTensor.Metrics.Pre
public import Physlib.Relativity.Tensors.RealTensor.ToComplex
public import Physlib.Relativity.Tensors.RealTensor.Units.Pre
public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules
public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic
public import Physlib.Relativity.Tensors.TensorSpecies.Basic
public import Physlib.Relativity.Tensors.Tensorial
public import Physlib.Relativity.Tensors.UnitTensor
public import Physlib.SpaceAndTime.Space.Basic
public import Physlib.SpaceAndTime.Space.ConstantSliceDist
public import Physlib.SpaceAndTime.Space.CrossProduct
public import Physlib.SpaceAndTime.Space.Derivatives.Basic
public import Physlib.SpaceAndTime.Space.Derivatives.Curl
public import Physlib.SpaceAndTime.Space.Derivatives.Div
public import Physlib.SpaceAndTime.Space.Derivatives.Grad
public import Physlib.SpaceAndTime.Space.Derivatives.Iterated
public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
public import Physlib.SpaceAndTime.Space.DistConst
public import Physlib.SpaceAndTime.Space.DistOfFunction
public import Physlib.SpaceAndTime.Space.Integrals.Basic
public import Physlib.SpaceAndTime.Space.Integrals.NormPow
public import Physlib.SpaceAndTime.Space.Integrals.RadialAngularMeasure
public import Physlib.SpaceAndTime.Space.IsDistBounded
public import Physlib.SpaceAndTime.Space.LengthUnit
public import Physlib.SpaceAndTime.Space.Module
public import Physlib.SpaceAndTime.Space.Norm
public import Physlib.SpaceAndTime.Space.Slice
public import Physlib.SpaceAndTime.Space.Translations
public import Physlib.SpaceAndTime.SpaceTime.Basic
public import Physlib.SpaceAndTime.SpaceTime.Boosts
public import Physlib.SpaceAndTime.SpaceTime.Derivatives
public import Physlib.SpaceAndTime.SpaceTime.LorentzAction
public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
public import Physlib.SpaceAndTime.Time.Basic
public import Physlib.SpaceAndTime.Time.Derivatives
public import Physlib.SpaceAndTime.Time.TimeMan
public import Physlib.SpaceAndTime.Time.TimeTransMan
public import Physlib.SpaceAndTime.Time.TimeUnit
public import Physlib.SpaceAndTime.TimeAndSpace.Basic
public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist
public import Physlib.StatisticalMechanics.BoltzmannConstant
public import Physlib.StatisticalMechanics.CanonicalEnsemble.Basic
public import Physlib.StatisticalMechanics.CanonicalEnsemble.Finite
public import Physlib.StatisticalMechanics.CanonicalEnsemble.Lemmas
public import Physlib.StatisticalMechanics.CanonicalEnsemble.TwoState
public import Physlib.StringTheory.Basic
public import Physlib.StringTheory.FTheory.SU5.Basic
public import Physlib.StringTheory.FTheory.SU5.Charges.AnomalyFree
public import Physlib.StringTheory.FTheory.SU5.Charges.OfRationalSection
public import Physlib.StringTheory.FTheory.SU5.Charges.Viable
public import Physlib.StringTheory.FTheory.SU5.Fluxes.Basic
public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
public import Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
public import Physlib.StringTheory.FTheory.SU5.Quanta.Basic
public import Physlib.StringTheory.FTheory.SU5.Quanta.FiveQuanta
public import Physlib.StringTheory.FTheory.SU5.Quanta.IsViable
public import Physlib.StringTheory.FTheory.SU5.Quanta.TenQuanta
public import Physlib.Thermodynamics.Basic
public import Physlib.Thermodynamics.IdealGas.Basic
public import Physlib.Thermodynamics.Temperature.Basic
public import Physlib.Thermodynamics.Temperature.TemperatureUnits
public import Physlib.Units.Basic
public import Physlib.Units.Dimension
public import Physlib.Units.Examples
public import Physlib.Units.FDeriv
public import Physlib.Units.Integral
public import Physlib.Units.UnitDependent
public import Physlib.Units.WithDim.Area
public import Physlib.Units.WithDim.Basic
public import Physlib.Units.WithDim.Energy
public import Physlib.Units.WithDim.Mass
public import Physlib.Units.WithDim.Momentum
public import Physlib.Units.WithDim.Pressure
public import Physlib.Units.WithDim.Speed
public import Physlib.Units.WithDim.Velocity