OAI/RepresentationTheory/RestrictedTilting/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 89 imports below, so a file that imports it gets all of them.
Imports
- OAI.RepresentationTheory.RestrictedTilting.AdicJets
- OAI.RepresentationTheory.RestrictedTilting.AssociatedBundle
- OAI.RepresentationTheory.RestrictedTilting.AssociatedFibre
- OAI.RepresentationTheory.RestrictedTilting.AssociatedNumerator
- OAI.RepresentationTheory.RestrictedTilting.AssociatedPlaneJet
- OAI.RepresentationTheory.RestrictedTilting.AssociatedProjective
- OAI.RepresentationTheory.RestrictedTilting.BaseChangeProjective
- OAI.RepresentationTheory.RestrictedTilting.BoundedOrigin
- OAI.RepresentationTheory.RestrictedTilting.BoundedOriginTarget
- OAI.RepresentationTheory.RestrictedTilting.BoundedStableFaithfulness
- OAI.RepresentationTheory.RestrictedTilting.BoundedUnipotentTilting
- OAI.RepresentationTheory.RestrictedTilting.BoundedWeightsFactors
- OAI.RepresentationTheory.RestrictedTilting.ClearedPolynomial
- OAI.RepresentationTheory.RestrictedTilting.CompatibleJets
- OAI.RepresentationTheory.RestrictedTilting.CompletedCoordinates
- OAI.RepresentationTheory.RestrictedTilting.CompletionCoefficients
- OAI.RepresentationTheory.RestrictedTilting.CompletionTriviality
- OAI.RepresentationTheory.RestrictedTilting.CoordinateTensor
- OAI.RepresentationTheory.RestrictedTilting.FaithfulTarget
- OAI.RepresentationTheory.RestrictedTilting.FiniteFreeTrace
- OAI.RepresentationTheory.RestrictedTilting.FiniteGenerator
- OAI.RepresentationTheory.RestrictedTilting.FiniteJetMaps
- OAI.RepresentationTheory.RestrictedTilting.FiniteSubgroupLift
- OAI.RepresentationTheory.RestrictedTilting.FormalAssociatedAction
- OAI.RepresentationTheory.RestrictedTilting.FormalAssociatedIso
- OAI.RepresentationTheory.RestrictedTilting.FormalLine
- OAI.RepresentationTheory.RestrictedTilting.FormalLineContinuity
- OAI.RepresentationTheory.RestrictedTilting.FormalSectionAction
- OAI.RepresentationTheory.RestrictedTilting.FormalSections
- OAI.RepresentationTheory.RestrictedTilting.GeneratedStableKernel
- OAI.RepresentationTheory.RestrictedTilting.GoodKernel
- OAI.RepresentationTheory.RestrictedTilting.GoodKernelExtension
- OAI.RepresentationTheory.RestrictedTilting.IntertwinerDescent
- OAI.RepresentationTheory.RestrictedTilting.JetTriviality
- OAI.RepresentationTheory.RestrictedTilting.LatticeLocalProjectivity
- OAI.RepresentationTheory.RestrictedTilting.LatticeNumerator
- OAI.RepresentationTheory.RestrictedTilting.LatticeSwap
- OAI.RepresentationTheory.RestrictedTilting.LaurentPolynomialSeparation
- OAI.RepresentationTheory.RestrictedTilting.LinearFormalComparison
- OAI.RepresentationTheory.RestrictedTilting.LowDegreeTrace
- OAI.RepresentationTheory.RestrictedTilting.Basic
- OAI.RepresentationTheory.RestrictedTilting.MatrixFormalComparison
- OAI.RepresentationTheory.RestrictedTilting.NormConverse
- OAI.RepresentationTheory.RestrictedTilting.NormDefinitions
- OAI.RepresentationTheory.RestrictedTilting.NormFree
- OAI.RepresentationTheory.RestrictedTilting.NormMaps
- OAI.RepresentationTheory.RestrictedTilting.NormProjectivity
- OAI.RepresentationTheory.RestrictedTilting.NumeratorAction
- OAI.RepresentationTheory.RestrictedTilting.PGroupInvariants
- OAI.RepresentationTheory.RestrictedTilting.PiPlaneOrigin
- OAI.RepresentationTheory.RestrictedTilting.PlaneFibre
- OAI.RepresentationTheory.RestrictedTilting.PlaneMatrixTensor
- OAI.RepresentationTheory.RestrictedTilting.PolynomialCovers
- OAI.RepresentationTheory.RestrictedTilting.PolynomialIntertwiner
- OAI.RepresentationTheory.RestrictedTilting.PolynomialJets
- OAI.RepresentationTheory.RestrictedTilting.ProjectiveFactor
- OAI.RepresentationTheory.RestrictedTilting.ProjectiveRegular
- OAI.RepresentationTheory.RestrictedTilting.RationalHomWeights
- OAI.RepresentationTheory.RestrictedTilting.RationalMatrices
- OAI.RepresentationTheory.RestrictedTilting.RegularSplitting
- OAI.RepresentationTheory.RestrictedTilting.RelativeTrace
- OAI.RepresentationTheory.RestrictedTilting.RepProducts
- OAI.RepresentationTheory.RestrictedTilting.RestrictedLift
- OAI.RepresentationTheory.RestrictedTilting.RestrictedTarget
- OAI.RepresentationTheory.RestrictedTilting.RestrictedTilting
- OAI.RepresentationTheory.RestrictedTilting.SmallGroupTrace
- OAI.RepresentationTheory.RestrictedTilting.SpecializeCompletion
- OAI.RepresentationTheory.RestrictedTilting.SplitRepresentation
- OAI.RepresentationTheory.RestrictedTilting.StableKernel
- OAI.RepresentationTheory.RestrictedTilting.StableRestriction
- OAI.RepresentationTheory.RestrictedTilting.SteinbergRegular
- OAI.RepresentationTheory.RestrictedTilting.SteinbergSpan
- OAI.RepresentationTheory.RestrictedTilting.TensorAssociatedAction
- OAI.RepresentationTheory.RestrictedTilting.TensorAssociatedIso
- OAI.RepresentationTheory.RestrictedTilting.TensorCoordinates
- OAI.RepresentationTheory.RestrictedTilting.TensorExactness
- OAI.RepresentationTheory.RestrictedTilting.TensorFormalComparison
- OAI.RepresentationTheory.RestrictedTilting.TensorNumerator
- OAI.RepresentationTheory.RestrictedTilting.TensorPlaneTilting
- OAI.RepresentationTheory.RestrictedTilting.TensorWeights
- OAI.RepresentationTheory.RestrictedTilting.ThetaTarget
- OAI.RepresentationTheory.RestrictedTilting.TiltingCovers
- OAI.RepresentationTheory.RestrictedTilting.TorusExtension
- OAI.RepresentationTheory.RestrictedTilting.TorusRelations
- OAI.RepresentationTheory.RestrictedTilting.TorusWeightProjection
- OAI.RepresentationTheory.RestrictedTilting.TraceFactor
- OAI.RepresentationTheory.RestrictedTilting.UnitAnnihilator
- OAI.RepresentationTheory.RestrictedTilting.UnitSimple
- OAI.RepresentationTheory.RestrictedTilting.XChartLineEval