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