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