Physlib/ClassicalMechanics/Basic.lean
Physlib/ClassicalMechanics/EulerLagrange.lean
Physlib/ClassicalMechanics/Force.lean
Physlib/ClassicalMechanics/FreeParticle/Basic.lean
Physlib/ClassicalMechanics/HamiltonianMechanics/HamiltonsEquations.lean
Physlib/ClassicalMechanics/HarmonicOscillator/WithDim.lean
Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
Physlib/ClassicalMechanics/Mass/MassUnit.lean
Physlib/ClassicalMechanics/OrbitalMechanics/VisViva.lean
Physlib/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean
Physlib/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean
Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean
Physlib/ClassicalMechanics/PointParticle/Basic.lean
Physlib/ClassicalMechanics/PointParticle/NewtonianSystem/Basic.lean
Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean
Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean
Physlib/ClassicalMechanics/RigidBody/Basic.lean
Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean
Physlib/ClassicalMechanics/RigidBody/Motion.lean
Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean
Physlib/ClassicalMechanics/Scattering/RigidSphere.lean
Physlib/ClassicalMechanics/Vibrations/LinearTriatomic.lean
Physlib/ClassicalMechanics/WaveEquation/HarmonicWave.lean
Physlib/CondensedMatter/BandTheory/Basic.lean
Physlib/CondensedMatter/Basic.lean
Physlib/CondensedMatter/LatticeModels/Basic.lean
Physlib/CondensedMatter/ManyBody/Basic.lean
Physlib/CondensedMatter/Response/Basic.lean
Physlib/CondensedMatter/Topology/Basic.lean
Physlib/Cosmology/Basic.lean
Physlib/Cosmology/FLRW/Basic.lean
Physlib/Cosmology/FLRW/ConformalTime.lean
Physlib/Cosmology/FLRW/DensityParameters.lean
Physlib/Cosmology/FLRW/Distances.lean
Physlib/Cosmology/FLRW/Dynamics.lean
Physlib/Cosmology/FLRW/MatterContent.lean
Physlib/Cosmology/FLRW/Solutions.lean
Physlib/Electromagnetism/Basic.lean
Physlib/Electromagnetism/Charge/ChargeUnit.lean
Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean
Physlib/Electromagnetism/Dynamics/IsExtrema.lean
Physlib/Electromagnetism/Kinematics/EMPotential.lean
Physlib/Electromagnetism/Kinematics/ElectricField.lean
Physlib/Electromagnetism/Kinematics/FieldStrength.lean
Physlib/Electromagnetism/Kinematics/MagneticField.lean
Physlib/Electromagnetism/Kinematics/ScalarPotential.lean
Physlib/Electromagnetism/Kinematics/VectorPotential.lean
Physlib/Electromagnetism/PointParticle/OneDimension.lean
Physlib/Electromagnetism/ThreeDimension/Basic.lean
Physlib/Electromagnetism/ThreeDimension/MaxwellEquations.lean
Physlib/LatticeQFT/Basic.lean
Physlib/Mathematics/Calculus/AdjFDeriv.lean
Physlib/Mathematics/Calculus/Divergence.lean
Physlib/Mathematics/Calculus/ParametricIntegration.lean
Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean
Physlib/Mathematics/Distribution/Basic.lean
Physlib/Mathematics/Distribution/PowMul.lean
Physlib/Mathematics/ForMathlib/DataStructures/Matrix/LieTrace.lean
Physlib/Mathematics/ForMathlib/FDerivCurry.lean
Physlib/Mathematics/ForMathlib/Fin.lean
Physlib/Mathematics/ForMathlib/Fin/Involutions.lean
Physlib/Mathematics/ForMathlib/HasTemperateGrowth.lean
Physlib/Mathematics/ForMathlib/LinearMaps.lean
Physlib/Mathematics/ForMathlib/List.lean
Physlib/Mathematics/ForMathlib/List/InsertIdx.lean
Physlib/Mathematics/ForMathlib/List/InsertionSort.lean
Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Basic.lean
Physlib/Mathematics/ForMathlib/OneParameterSubgroups/Unitary.lean
Physlib/Mathematics/ForMathlib/OrthogonalMatrix.lean
Physlib/Mathematics/ForMathlib/SchurTriangulation.lean
Physlib/Mathematics/ForMathlib/Trigonometry/Tanh.lean
Physlib/Mathematics/Groups/SO3/Basic.lean
Physlib/Mathematics/InnerProductSpace/Adjoint.lean
Physlib/Mathematics/InnerProductSpace/Basic.lean
Physlib/Mathematics/InnerProductSpace/Calculus.lean
Physlib/Mathematics/InnerProductSpace/Submodule.lean
Physlib/Mathematics/Modules/ConjModule.lean
Physlib/Mathematics/Modules/CrossProduct.lean
Physlib/Mathematics/Modules/CrossProductMatrix.lean
Physlib/Mathematics/SpecialFunctions/PhysHermite.lean
Physlib/Mathematics/VariationalCalculus/Basic.lean
Physlib/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean
Physlib/Mathematics/VariationalCalculus/HasVarAdjoint.lean
Physlib/Mathematics/VariationalCalculus/HasVarGradient.lean
Physlib/Mathematics/VariationalCalculus/IsLocalizedfunctionTransform.lean
Physlib/Mathematics/VariationalCalculus/IsTestFunction.lean
Physlib/Meta/AllFilePaths.lean
Physlib/Meta/Basic.lean
Physlib/Meta/Informal/Basic.lean
Physlib/Meta/Informal/Post.lean
Physlib/Meta/Informal/SemiFormal.lean
Physlib/Meta/Linters/DefsWithUnderscore.lean
Physlib/Meta/Linters/Sorry.lean
Physlib/Meta/Notes/Basic.lean
Physlib/Meta/Notes/HTMLNote.lean
Physlib/Meta/Notes/NoteFile.lean
Physlib/Meta/Notes/ToHTML.lean
Physlib/Meta/Remark/Basic.lean
Physlib/Meta/Remark/Properties.lean
Physlib/Meta/TODO/Basic.lean
Physlib/Meta/TODO/Global.lean
Physlib/Meta/TransverseTactics.lean
Physlib/Optics/Basic.lean
Physlib/Optics/Polarization/Basic.lean
Physlib/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
Physlib/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/NoGrav/Basic.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Ordinary/Basic.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Ordinary/DimSevenPlane.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Ordinary/FamilyMaps.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Permutations.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/BMinusL.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/Basic.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/BoundPlaneDim.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/FamilyMaps.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/PlaneNonSols.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol.lean
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSolToSol.lean
Physlib/Particles/BeyondTheStandardModel/Spin10/Basic.lean
Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/Basic.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/Invariants.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/Relations.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/Rows.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
Physlib/Particles/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
Physlib/Particles/NeutrinoPhysics/Basic.lean
Physlib/Particles/StandardModel/AnomalyCancellation/Basic.lean
Physlib/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean
Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/Basic.lean
Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
Physlib/Particles/StandardModel/AnomalyCancellation/Permutations.lean
Physlib/Particles/StandardModel/Basic.lean
Physlib/Particles/StandardModel/Fermions/DownSinglet.lean
Physlib/Particles/StandardModel/Fermions/LeptonDoublet.lean
Physlib/Particles/StandardModel/Fermions/LeptonSinglet.lean
Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
Physlib/Particles/StandardModel/Fermions/UpSinglet.lean
Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean
Physlib/Particles/StandardModel/HiggsBoson/Potential.lean
Physlib/Particles/StandardModel/Representations.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/HyperCharge.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Permutations.lean
Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Y3.lean
Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean
Physlib/ProbabilisticTheory/OrderUnit/Basic.lean
Physlib/ProbabilisticTheory/OrderUnit/Cone.lean
Physlib/QFT/AnomalyCancellation/GroupActions.lean
Physlib/QFT/PerturbationTheory/CreateAnnihilate.lean
Physlib/QFT/PerturbationTheory/FeynmanDiagrams/Basic.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/NormTimeOrder.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/Basic.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/Filters.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/NormalOrder.lean
Physlib/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean
Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean
Physlib/QFT/PerturbationTheory/FieldStatistics/ExchangeSign.lean
Physlib/QFT/PerturbationTheory/FieldStatistics/OfFinset.lean
Physlib/QFT/PerturbationTheory/Koszul/KoszulSign.lean
Physlib/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/Grading.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/NormalOrder/Basic.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/NormalOrder/Lemmas.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/NormalOrder/WickContractions.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/StaticWickTerm.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/StaticWickTheorem.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/SuperCommute.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/TimeContraction.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/TimeOrder.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/Universality.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/WickTerm.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/WicksTheorem.lean
Physlib/QFT/PerturbationTheory/WickAlgebra/WicksTheoremNormal.lean
Physlib/QFT/PerturbationTheory/WickContraction/Basic.lean
Physlib/QFT/PerturbationTheory/WickContraction/Card.lean
Physlib/QFT/PerturbationTheory/WickContraction/Erase.lean
Physlib/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean
Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContract.lean
Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean
Physlib/QFT/PerturbationTheory/WickContraction/Involutions.lean
Physlib/QFT/PerturbationTheory/WickContraction/IsFull.lean
Physlib/QFT/PerturbationTheory/WickContraction/Join.lean
Physlib/QFT/PerturbationTheory/WickContraction/Perm.lean
Physlib/QFT/PerturbationTheory/WickContraction/Sign/Basic.lean
Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertNone.lean
Physlib/QFT/PerturbationTheory/WickContraction/Sign/InsertSome.lean
Physlib/QFT/PerturbationTheory/WickContraction/Sign/Join.lean
Physlib/QFT/PerturbationTheory/WickContraction/Singleton.lean
Physlib/QFT/PerturbationTheory/WickContraction/StaticContract.lean
Physlib/QFT/PerturbationTheory/WickContraction/SubContraction.lean
Physlib/QFT/PerturbationTheory/WickContraction/TimeCond.lean
Physlib/QFT/PerturbationTheory/WickContraction/TimeContract.lean
Physlib/QFT/PerturbationTheory/WickContraction/Uncontracted.lean
Physlib/QFT/PerturbationTheory/WickContraction/UncontractedList.lean
Physlib/QFT/QED/AnomalyCancellation/Basic.lean
Physlib/QFT/QED/AnomalyCancellation/BasisLinear.lean
Physlib/QFT/QED/AnomalyCancellation/ConstAbs.lean
Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean
Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean
Physlib/QFT/QED/AnomalyCancellation/LineInPlaneCond.lean
Physlib/QFT/QED/AnomalyCancellation/LowDim/One.lean
Physlib/QFT/QED/AnomalyCancellation/LowDim/Three.lean
Physlib/QFT/QED/AnomalyCancellation/LowDim/Two.lean
Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean
Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean
Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean
Physlib/QFT/QED/AnomalyCancellation/Permutations.lean
Physlib/QFT/QED/AnomalyCancellation/Sorts.lean
Physlib/QFT/QED/AnomalyCancellation/VectorLike.lean
Physlib/QuantumMechanics/FiniteTarget.lean
Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean
Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean
Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Completeness.lean
Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Eigenfunction.lean
Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Examples.lean
Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/TISE.lean
Physlib/QuantumMechanics/HilbertSpaces/FiniteTarget/Basic.lean
Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Basic.lean
Physlib/QuantumMechanics/HilbertSpaces/OneDimension/Gaussians.lean
Physlib/QuantumMechanics/HilbertSpaces/OneDimension/PlaneWaves.lean
Physlib/QuantumMechanics/HilbertSpaces/OneDimension/PositionStates.lean
Physlib/QuantumMechanics/HilbertSpaces/OneDimension/SchwartzSubmodule.lean
Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean
Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean
Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean
Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
Physlib/QuantumMechanics/Hydrogen/Basic.lean
Physlib/QuantumMechanics/Hydrogen/LaplaceRungeLenzVector.lean
Physlib/QuantumMechanics/Operators/AngularMomentum.lean
Physlib/QuantumMechanics/Operators/Examples.lean
Physlib/QuantumMechanics/Operators/OneDimension/Commutation.lean
Physlib/QuantumMechanics/Operators/OneDimension/Momentum.lean
Physlib/QuantumMechanics/Operators/OneDimension/Parity.lean
Physlib/QuantumMechanics/Operators/OneDimension/Position.lean
Physlib/QuantumMechanics/Operators/OneDimension/Unbounded.lean
Physlib/QuantumMechanics/Operators/Position.lean
Physlib/QuantumMechanics/Operators/StateObservables/ExpectedValue.lean
Physlib/QuantumMechanics/Operators/StateObservables/IsEigenvector.lean
Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean
Physlib/QuantumMechanics/Operators/Unbounded.lean
Physlib/QuantumMechanics/PlanckConstant.lean
Physlib/Relativity/Bispinors/Basic.lean
Physlib/Relativity/Causality/Basic.lean
Physlib/Relativity/Causality/CausallyFollows.lean
Physlib/Relativity/Causality/LightLike.lean
Physlib/Relativity/Causality/TimeLike.lean
Physlib/Relativity/CliffordAlgebra.lean
Physlib/Relativity/Fermions/Dirac/Basic.lean
Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean
Physlib/Relativity/Fermions/Dirac/Slash.lean
Physlib/Relativity/Fermions/Weyl/Contraction.lean
Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean
Physlib/Relativity/Fermions/Weyl/Duals.lean
Physlib/Relativity/Fermions/Weyl/LeftHanded.lean
Physlib/Relativity/Fermions/Weyl/Metric.lean
Physlib/Relativity/Fermions/Weyl/RightHanded.lean
Physlib/Relativity/Fermions/Weyl/Two.lean
Physlib/Relativity/Fermions/Weyl/Unit.lean
Physlib/Relativity/LorentzAlgebra/Basic.lean
Physlib/Relativity/LorentzAlgebra/Basis.lean
Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean
Physlib/Relativity/LorentzGroup/Basic.lean
Physlib/Relativity/LorentzGroup/Boosts/Apply.lean
Physlib/Relativity/LorentzGroup/Boosts/Axis.lean
Physlib/Relativity/LorentzGroup/Boosts/Basic.lean
Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean
Physlib/Relativity/LorentzGroup/Orthochronous/Basic.lean
Physlib/Relativity/LorentzGroup/Proper.lean
Physlib/Relativity/LorentzGroup/Restricted/Basic.lean
Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean
Physlib/Relativity/LorentzGroup/Rotations.lean
Physlib/Relativity/LorentzGroup/ToVector.lean
Physlib/Relativity/PauliMatrices/AsTensor.lean
Physlib/Relativity/PauliMatrices/Basic.lean
Physlib/Relativity/PauliMatrices/CliffordAlgebra.lean
Physlib/Relativity/PauliMatrices/Relations.lean
Physlib/Relativity/PauliMatrices/SelfAdjoint.lean
Physlib/Relativity/PauliMatrices/ToTensor.lean
Physlib/Relativity/SL2C/AxisRotations.lean
Physlib/Relativity/SL2C/Basic.lean
Physlib/Relativity/SL2C/SelfAdjoint.lean
Physlib/Relativity/Special/ProperTime.lean
Physlib/Relativity/Special/TwinParadox/Basic.lean
Physlib/Relativity/Tensors/Basic.lean
Physlib/Relativity/Tensors/ComplexTensor/Basic.lean
Physlib/Relativity/Tensors/ComplexTensor/Lemmas.lean
Physlib/Relativity/Tensors/ComplexTensor/Matrix/Pre.lean
Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean
Physlib/Relativity/Tensors/ComplexTensor/Metrics/Lemmas.lean
Physlib/Relativity/Tensors/ComplexTensor/Metrics/Pre.lean
Physlib/Relativity/Tensors/ComplexTensor/OfGaussianInt.lean
Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean
Physlib/Relativity/Tensors/ComplexTensor/Units/Pre.lean
Physlib/Relativity/Tensors/ComplexTensor/Units/Symm.lean
Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean
Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Contraction.lean
Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Modules.lean
Physlib/Relativity/Tensors/Conjugation/Basic.lean
Physlib/Relativity/Tensors/Constructors.lean
Physlib/Relativity/Tensors/Contraction/Basic.lean
Physlib/Relativity/Tensors/Contraction/Basis.lean
Physlib/Relativity/Tensors/Contraction/Products.lean
Physlib/Relativity/Tensors/Contraction/Pure.lean
Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
Physlib/Relativity/Tensors/Dual.lean
Physlib/Relativity/Tensors/Elab.lean
Physlib/Relativity/Tensors/Evaluation.lean
Physlib/Relativity/Tensors/LeviCivita/Complex.lean
Physlib/Relativity/Tensors/MetricTensor.lean
Physlib/Relativity/Tensors/OfInt.lean
Physlib/Relativity/Tensors/Product.lean
Physlib/Relativity/Tensors/RealTensor/Basic.lean
Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean
Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean
Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean
Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean
Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean
Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean
Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean
Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Modules.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean
Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean
Physlib/Relativity/Tensors/RealTensor/Velocity/Basic.lean
Physlib/Relativity/Tensors/Reindexing.lean
Physlib/Relativity/Tensors/TensorSpecies/Basic.lean
Physlib/Relativity/Tensors/UnitTensor.lean
Physlib/SpaceAndTime/GalileanGroup/Basic.lean
Physlib/SpaceAndTime/ReferenceFrame.lean
Physlib/SpaceAndTime/Space/Basic.lean
Physlib/SpaceAndTime/Space/Derivatives/Basic.lean
Physlib/SpaceAndTime/Space/Derivatives/Curl.lean
Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
Physlib/SpaceAndTime/Space/EuclideanGroup/Action.lean
Physlib/SpaceAndTime/Space/EuclideanGroup/AffineGroup.lean
Physlib/SpaceAndTime/Space/EuclideanGroup/Basic.lean
Physlib/SpaceAndTime/Space/Integrals/Basic.lean
Physlib/SpaceAndTime/Space/Integrals/NormPow.lean
Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
Physlib/SpaceAndTime/Space/LengthUnit.lean
Physlib/SpaceAndTime/Space/Module.lean
Physlib/SpaceAndTime/Space/Origin.lean
Physlib/SpaceAndTime/Space/SmoothFunctions.lean
Physlib/SpaceAndTime/Space/Translations.lean
Physlib/SpaceAndTime/SpaceTime/TimeSlice.lean
Physlib/SpaceAndTime/Time/Basic.lean
Physlib/SpaceAndTime/Time/MatrixDerivatives.lean
Physlib/SpaceAndTime/Time/TimeMan.lean
Physlib/SpaceAndTime/Time/TimeUnit.lean
Physlib/StatisticalMechanics/BoltzmannConstant.lean
Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean
Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean
Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean
Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean
Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean
Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean
Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean
Physlib/StringTheory/Basic.lean
Physlib/StringTheory/FTheory/SU5/Basic.lean
Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean
Physlib/Thermodynamics/Basic.lean
Physlib/Thermodynamics/IdealGas/Basic.lean
Physlib/Thermodynamics/Temperature/Basic.lean
Physlib/Thermodynamics/Temperature/TemperatureUnits.lean
Physlib/Units/Basic.lean
Physlib/Units/Dimension.lean
Physlib/Units/Examples.lean
Physlib/Units/Exponent.lean
Physlib/Units/FDeriv.lean
Physlib/Units/ISQBridge.lean
Physlib/Units/ISQDimensionBase.lean
Physlib/Units/Integral.lean
Physlib/Units/LTMCTDimensionBase.lean
Physlib/Units/ParametricDimensionExamples.lean
Physlib/Units/ParametricUnits.lean
Physlib/Units/PositiveRealUnit.lean
Physlib/Units/SIUnitChoices.lean
Physlib/Units/UnitDependent.lean
Physlib/Units/UnitSystem.lean
Physlib/Units/WithDim/Analysis.lean
Physlib/Units/WithDim/Area.lean
Physlib/Units/WithDim/Basic.lean
Physlib/Units/WithDim/Energy.lean
Physlib/Units/WithDim/Mass.lean
Physlib/Units/WithDim/Momentum.lean
Physlib/Units/WithDim/Pressure.lean
Physlib/Units/WithDim/Speed.lean
Physlib/Units/WithDim/Velocity.lean
QuantumInfo/ForMathlib/ContinuousLinearMap.lean
QuantumInfo/ForMathlib/HayataGroup/TraceInequality/BlockDiagonal.lean
QuantumInfo/ForMathlib/HermitianMat.lean
QuantumInfo/ForMathlib/HermitianMat/CompoundMatrix.lean
QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean
QuantumInfo/ForMathlib/Tactic/Commutes.lean
QuantumInfo/ForMathlib/Tactic/Commutes/Attribute.lean
QuantumInfo/ForMathlib/ULift.lean
QuantumInfo/Operators/Unitary.lean
QuantumInfo/States/Pure/BargmannInvariant.lean
