-
Notifications
You must be signed in to change notification settings - Fork 146
Expand file tree
/
Copy pathPhyslib.lean
More file actions
531 lines (530 loc) · 32.9 KB
/
Copy pathPhyslib.lean
File metadata and controls
531 lines (530 loc) · 32.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
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
module
public import Physlib.ClassicalFieldTheory.Local.Variation
public import Physlib.ClassicalMechanics.Basic
public import Physlib.ClassicalMechanics.DampedHarmonicOscillator.Basic
public import Physlib.ClassicalMechanics.DampedHarmonicOscillator.Solution
public import Physlib.ClassicalMechanics.EulerLagrange
public import Physlib.ClassicalMechanics.FreeParticle.Basic
public import Physlib.ClassicalMechanics.HamiltonsEquations
public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic
public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic
public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.KineticEnergy
public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Trajectory
public import Physlib.ClassicalMechanics.HarmonicOscillator.Solution
public import Physlib.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
public import Physlib.ClassicalMechanics.Mass.MassUnit
public import Physlib.ClassicalMechanics.OrbitalMechanics.VisViva
public import Physlib.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
public import Physlib.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum
public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
public import Physlib.ClassicalMechanics.RigidBody.Basic
public import Physlib.ClassicalMechanics.RigidBody.KineticEnergy
public import Physlib.ClassicalMechanics.RigidBody.Motion
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.Thermoelectric.Basic
public import Physlib.CondensedMatter.TightBindingChain.Basic
public import Physlib.Cosmology.Basic
public import Physlib.Cosmology.FLRW.Basic
public import Physlib.Cosmology.FLRW.ConformalTime
public import Physlib.Cosmology.FLRW.DensityParameters
public import Physlib.Cosmology.FLRW.Distances
public import Physlib.Cosmology.FLRW.Dynamics
public import Physlib.Cosmology.FLRW.MatterContent
public import Physlib.Cosmology.FLRW.Solutions
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.Distributional.Basic
public import Physlib.Electromagnetism.Distributional.Dynamics.CurrentDensity
public import Physlib.Electromagnetism.Distributional.Dynamics.IsExtrema
public import Physlib.Electromagnetism.Distributional.Dynamics.KineticTerm
public import Physlib.Electromagnetism.Distributional.Dynamics.Lagrangian
public import Physlib.Electromagnetism.Distributional.ElectricField
public import Physlib.Electromagnetism.Distributional.FieldStrength
public import Physlib.Electromagnetism.Distributional.MagneticField
public import Physlib.Electromagnetism.Distributional.ScalarPotential
public import Physlib.Electromagnetism.Distributional.VectorPotential
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.GaugeTransformation
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.FluidDynamics.Basic
public import Physlib.FluidDynamics.CauchyFlow.Basic
public import Physlib.FluidDynamics.CauchyFlow.BodyForce
public import Physlib.FluidDynamics.CauchyFlow.Inviscid
public import Physlib.FluidDynamics.CauchyFlow.Momentum
public import Physlib.FluidDynamics.CauchyFlow.NavierStokes
public import Physlib.FluidDynamics.CauchyFlow.Newtonian
public import Physlib.FluidDynamics.Euler.Basic
public import Physlib.FluidDynamics.FluidFlow.Basic
public import Physlib.FluidDynamics.FluidFlow.Continuity
public import Physlib.FluidDynamics.FluidFlow.Incompressible
public import Physlib.FluidDynamics.FluidFlow.Kinematics
public import Physlib.FluidDynamics.FluidFlow.Momentum
public import Physlib.FluidDynamics.FluidFlow.Newtonian
public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Basic
public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Bernoulli
public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Isentropic
public import Physlib.Mathematics.Calculus.AdjFDeriv
public import Physlib.Mathematics.Calculus.Divergence
public import Physlib.Mathematics.Calculus.ParametricIntegration
public import Physlib.Mathematics.Calculus.Wirtinger.Basic
public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
public import Physlib.Mathematics.ConjModule
public import Physlib.Mathematics.CrossProduct
public import Physlib.Mathematics.CrossProductMatrix
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.Basic
public import Physlib.Mathematics.KroneckerDelta.Contraction
public import Physlib.Mathematics.LinearMaps
public import Physlib.Mathematics.LinearPMap
public import Physlib.Mathematics.List
public import Physlib.Mathematics.List.InsertIdx
public import Physlib.Mathematics.List.InsertionSort
public import Physlib.Mathematics.OrthogonalMatrix
public import Physlib.Mathematics.PiTensorProduct
public import Physlib.Mathematics.RatComplexNum
public import Physlib.Mathematics.Resolvent
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.TODO.Global
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.Fermions.DownSinglet
public import Physlib.Particles.StandardModel.Fermions.LeptonDoublet
public import Physlib.Particles.StandardModel.Fermions.LeptonSinglet
public import Physlib.Particles.StandardModel.Fermions.QuarkDoublet
public import Physlib.Particles.StandardModel.Fermions.UpSinglet
public import Physlib.Particles.StandardModel.HiggsBoson.Basic
public import Physlib.Particles.StandardModel.HiggsBoson.EffectivePotential
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.N1.Basic
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.FiniteTarget
public import Physlib.QuantumMechanics.FreeParticle.Basic
public import Physlib.QuantumMechanics.HarmonicOscillator.Basic
public import Physlib.QuantumMechanics.HarmonicOscillator.LadderOperators
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Completeness
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Examples
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.TISE
public import Physlib.QuantumMechanics.HilbertSpaces.FiniteTarget.Basic
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Basic
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Gaussians
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.PlaneWaves
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.PositionStates
public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.SchwartzSubmodule
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Basic
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.DirichletSubmodule
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Fourier
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.PolyBddSchwartzSubmodule
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SobolevSubmodule
public import Physlib.QuantumMechanics.Hydrogen.Basic
public import Physlib.QuantumMechanics.Hydrogen.LaplaceRungeLenzVector
public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic
public import Physlib.QuantumMechanics.Operators.AngularMomentum
public import Physlib.QuantumMechanics.Operators.Commutation
public import Physlib.QuantumMechanics.Operators.Covariance
public import Physlib.QuantumMechanics.Operators.Examples
public import Physlib.QuantumMechanics.Operators.Momentum
public import Physlib.QuantumMechanics.Operators.Multiplication
public import Physlib.QuantumMechanics.Operators.OneDimension.Commutation
public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum
public import Physlib.QuantumMechanics.Operators.OneDimension.Parity
public import Physlib.QuantumMechanics.Operators.OneDimension.Position
public import Physlib.QuantumMechanics.Operators.OneDimension.Unbounded
public import Physlib.QuantumMechanics.Operators.Position
public import Physlib.QuantumMechanics.Operators.SpectralTheory.Basic
public import Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint
public import Physlib.QuantumMechanics.Operators.SpectralTheory.SpectralMeasure
public import Physlib.QuantumMechanics.Operators.SpectralTheory.Symmetric
public import Physlib.QuantumMechanics.Operators.StateObservables.ExpectedValue
public import Physlib.QuantumMechanics.Operators.StateObservables.IsEigenvector
public import Physlib.QuantumMechanics.Operators.StateObservables.Variance
public import Physlib.QuantumMechanics.Operators.Unbounded
public import Physlib.QuantumMechanics.Operators.Uncertainty
public import Physlib.QuantumMechanics.PlanckConstant
public import Physlib.QuantumMechanics.QuantumSystem.Basic
public import Physlib.QuantumMechanics.RectangularBarrier.Basic
public import Physlib.QuantumMechanics.ReflectionlessPotential.Basic
public import Physlib.QuantumMechanics.SpaceDQuantumSystem
public import Physlib.Relativity.Bispinors.Basic
public import Physlib.Relativity.CliffordAlgebra
public import Physlib.Relativity.Fermions.Dirac.Basic
public import Physlib.Relativity.Fermions.Weyl.Contraction
public import Physlib.Relativity.Fermions.Weyl.DualLeftHanded
public import Physlib.Relativity.Fermions.Weyl.DualRightHanded
public import Physlib.Relativity.Fermions.Weyl.Duals
public import Physlib.Relativity.Fermions.Weyl.LeftHanded
public import Physlib.Relativity.Fermions.Weyl.Metric
public import Physlib.Relativity.Fermions.Weyl.RightHanded
public import Physlib.Relativity.Fermions.Weyl.Two
public import Physlib.Relativity.Fermions.Weyl.Unit
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.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.ComponentIdx.Basic
public import Physlib.Relativity.Tensors.ComponentIdx.Contraction
public import Physlib.Relativity.Tensors.ComponentIdx.Product
public import Physlib.Relativity.Tensors.ComponentIdx.Single
public import Physlib.Relativity.Tensors.Conjugation.Basic
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.Contraction.SuccSuccAbove
public import Physlib.Relativity.Tensors.Dual
public import Physlib.Relativity.Tensors.Elab
public import Physlib.Relativity.Tensors.Evaluation
public import Physlib.Relativity.Tensors.LeviCivita.Basic
public import Physlib.Relativity.Tensors.LeviCivita.Contractions
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.CoVector.Representation
public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial
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.Representation.Contraction
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.Vector.Representation
public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial
public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic
public import Physlib.Relativity.Tensors.Reindexing
public import Physlib.Relativity.Tensors.TensorSpecies.Basic
public import Physlib.Relativity.Tensors.Tensorial
public import Physlib.Relativity.Tensors.UnitTensor
public import Physlib.SpaceAndTime.GalileanGroup.Basic
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.DerivativeIndex
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.MatrixDiv
public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
public import Physlib.SpaceAndTime.Space.DistConst
public import Physlib.SpaceAndTime.Space.DistOfFunction
public import Physlib.SpaceAndTime.Space.EuclideanGroup.Action
public import Physlib.SpaceAndTime.Space.EuclideanGroup.AffineGroup
public import Physlib.SpaceAndTime.Space.EuclideanGroup.Basic
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.Basic
public import Physlib.SpaceAndTime.Space.Norm.IteratedLaplacian
public import Physlib.SpaceAndTime.Space.Norm.Regularized
public import Physlib.SpaceAndTime.Space.Origin
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.MatrixDerivatives
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.SpaceAndTime.TimeAndSpace.EuclideanGroup.Action
public import Physlib.SpaceAndTime.TimeAndSpace.EuclideanGroup.SchwartzAction
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.StatisticalMechanics.MicroCanonicalEnsemble.Basic
public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.IdealGas
public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantities
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.ISQBridge
public import Physlib.Units.ISQDimensionBase
public import Physlib.Units.Integral
public import Physlib.Units.LTMCTDimensionBase
public import Physlib.Units.ParametricDimensionExamples
public import Physlib.Units.ParametricUnits
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