OAI/MathematicalPhysics/BFSS/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 73 imports below, so a file that imports it gets all of them.
Imports
- OAI.MathematicalPhysics.BFSS.Core
- OAI.MathematicalPhysics.BFSS.CliffordSymbols
- OAI.MathematicalPhysics.BFSS.Cutoffs
- OAI.MathematicalPhysics.BFSS.Kinetic
- OAI.MathematicalPhysics.BFSS.GammaWords
- OAI.MathematicalPhysics.BFSS.GammaIdentity
- OAI.MathematicalPhysics.BFSS.MassIdentity
- OAI.MathematicalPhysics.BFSS.PotentialBasis
- OAI.MathematicalPhysics.BFSS.MassiveCoercivity
- OAI.MathematicalPhysics.BFSS.ColorMatrices
- OAI.MathematicalPhysics.BFSS.PotentialSquares
- OAI.MathematicalPhysics.BFSS.MixedEnergy
- OAI.MathematicalPhysics.BFSS.DeformedCharge
- OAI.MathematicalPhysics.BFSS.PotentialBounds
- OAI.MathematicalPhysics.BFSS.MassiveMoments
- OAI.MathematicalPhysics.BFSS.ColorLie
- OAI.MathematicalPhysics.BFSS.NormalCocycle
- OAI.MathematicalPhysics.BFSS.NormalPotential
- OAI.MathematicalPhysics.BFSS.NormalLinearization
- OAI.MathematicalPhysics.BFSS.TaylorBounds
- OAI.MathematicalPhysics.BFSS.GaugeGeometry
- OAI.MathematicalPhysics.BFSS.DistanceBounds
- OAI.MathematicalPhysics.BFSS.GaugeOrbits
- OAI.MathematicalPhysics.BFSS.NormalTubes
- OAI.MathematicalPhysics.BFSS.NormalCharts
- OAI.MathematicalPhysics.BFSS.SliceIntegrals
- OAI.MathematicalPhysics.BFSS.GaugeAverages
- OAI.MathematicalPhysics.BFSS.SliceDensity
- OAI.MathematicalPhysics.BFSS.OrbitDensity
- OAI.MathematicalPhysics.BFSS.GaugeCore
- OAI.MathematicalPhysics.BFSS.LocalBounds
- OAI.MathematicalPhysics.BFSS.RellichSmoothing
- OAI.MathematicalPhysics.BFSS.RellichCompactness
- OAI.MathematicalPhysics.BFSS.CoreCompactness
- OAI.MathematicalPhysics.BFSS.SmallPatches
- OAI.MathematicalPhysics.BFSS.MeasuredFields
- OAI.MathematicalPhysics.BFSS.OrbitCutoffs
- OAI.MathematicalPhysics.BFSS.NormExhaustion
- OAI.MathematicalPhysics.BFSS.WeightedCompactness
- OAI.MathematicalPhysics.BFSS.ProfileExtraction
- OAI.MathematicalPhysics.BFSS.ClosedProfiles
- OAI.MathematicalPhysics.BFSS.StabilizerProfiles
- OAI.MathematicalPhysics.BFSS.FiniteFamilies
- OAI.MathematicalPhysics.BFSS.WeakLimits
- OAI.MathematicalPhysics.BFSS.SobolevGraphs
- OAI.MathematicalPhysics.BFSS.LocalL2
- OAI.MathematicalPhysics.BFSS.WeightedGradients
- OAI.MathematicalPhysics.BFSS.ProfileMoments
- OAI.MathematicalPhysics.BFSS.KineticMeasures
- OAI.MathematicalPhysics.BFSS.SharpCutoffs
- OAI.MathematicalPhysics.BFSS.PotentialLimits
- OAI.MathematicalPhysics.BFSS.EnergyLimits
- OAI.MathematicalPhysics.BFSS.CovariantFields
- OAI.MathematicalPhysics.BFSS.ProfileEnergy
- OAI.MathematicalPhysics.BFSS.OscillatorLimits
- OAI.MathematicalPhysics.BFSS.EnergyExtraction
- OAI.MathematicalPhysics.BFSS.NormalFields
- OAI.MathematicalPhysics.BFSS.OscillatorForms
- OAI.MathematicalPhysics.BFSS.FormClosure
- OAI.MathematicalPhysics.BFSS.FormCompactness
- OAI.MathematicalPhysics.BFSS.LowerContinuity
- OAI.MathematicalPhysics.BFSS.NormalGap
- OAI.MathematicalPhysics.BFSS.SpinCoupling
- OAI.MathematicalPhysics.BFSS.FermionFrequency
- OAI.MathematicalPhysics.BFSS.FrequencyContraction
- OAI.MathematicalPhysics.BFSS.FermionQuantization
- OAI.MathematicalPhysics.BFSS.FrequencyComparison
- OAI.MathematicalPhysics.BFSS.FrequencyOperators
- OAI.MathematicalPhysics.BFSS.FermionModes
- OAI.MathematicalPhysics.BFSS.FrequencySpectrum
- OAI.MathematicalPhysics.BFSS.Vacuum
- OAI.MathematicalPhysics.BFSS.GroundLine
- OAI.MathematicalPhysics.BFSS.GroundEnergy