OAI/RepresentationTheory/RestrictedTilting/
1194 declarations, 0 contain sorry, 0 declared as axioms; 116 files
Files
- ActionDenominators.lean 6 declarations
- AdicJets.lean 7 declarations
- AssociatedBundle.lean 3 declarations
- AssociatedFibre.lean 5 declarations
- AssociatedLattices.lean 13 declarations
- AssociatedNumerator.lean 6 declarations
- AssociatedPlaneJet.lean 3 declarations
- AssociatedProjective.lean 1 declarations
- AssociatedWeights.lean 32 declarations
- BaseChangeProjective.lean 1 declarations
- Basic.lean 4 imports, no declarations
- BinarySequences.lean 37 declarations
- BoundedOrigin.lean 1 declarations
- BoundedOriginTarget.lean 7 declarations
- BoundedStableFaithfulness.lean 4 declarations
- BoundedUnipotentTilting.lean 1 declarations
- BoundedWeightsFactors.lean 1 declarations
- CharacterExpansions.lean 44 declarations
- ClearedPolynomial.lean 7 declarations
- CompatibleJets.lean 11 declarations
- CompletedCoordinates.lean 6 declarations
- CompletionCoefficients.lean 4 declarations
- CompletionTriviality.lean 2 declarations
- CoordinateTensor.lean 7 declarations
- DualSplitting.lean 17 declarations
- ExtensionSplitting.lean 24 declarations
- FaithfulTarget.lean 32 declarations
- FiniteFreeTrace.lean 7 declarations
- FiniteGenerator.lean 3 declarations
- FiniteJetMaps.lean 7 declarations
- FiniteSubgroupLift.lean 1 declarations
- FormalAssociatedAction.lean 4 declarations
- FormalAssociatedIso.lean 6 declarations
- FormalLine.lean 10 declarations
- FormalLineContinuity.lean 2 declarations
- FormalSectionAction.lean 1 declarations
- FormalSections.lean 10 declarations
- FrobeniusTensor.lean 18 declarations
- GeneratedStableKernel.lean 7 declarations
- GlobalLattices.lean 30 declarations
- GoodKernel.lean 10 declarations
- GoodKernelExtension.lean 2 declarations
- IntertwinerDescent.lean 2 declarations
- JetRelations.lean 30 declarations
- JetRepresentations.lean 40 declarations
- JetTriviality.lean 7 declarations
- LatticeGluing.lean 17 declarations
- LatticeLocalProjectivity.lean 1 declarations
- LatticeNumerator.lean 9 declarations
- LatticeSwap.lean 2 declarations
- LaurentPolynomialSeparation.lean 4 declarations
- LinearFormalComparison.lean 4 declarations
- LocalFreeness.lean 6 declarations
- LowDegreeTrace.lean 3 declarations
- Main.lean 89 imports, no declarations
- MatrixFormalComparison.lean 1 declarations
- NormConverse.lean 2 declarations
- NormDefinitions.lean 4 declarations
- NormFree.lean 7 declarations
- NormMaps.lean 4 declarations
- NormProjectivity.lean 2 declarations
- NumeratorAction.lean 2 declarations
- OriginCoordinates.lean 39 declarations
- PGroupInvariants.lean 1 declarations
- PiPlaneOrigin.lean 9 declarations
- PlaneCharts.lean 24 declarations
- PlaneFibre.lean 13 declarations
- PlaneMatrixTensor.lean 10 declarations
- PolynomialActions.lean 28 declarations
- PolynomialCovers.lean 9 declarations
- PolynomialIntertwiner.lean 2 declarations
- PolynomialJets.lean 8 declarations
- ProjectiveFactor.lean 5 declarations
- ProjectiveRegular.lean 2 declarations
- RationalHomWeights.lean 3 declarations
- RationalMatrices.lean 10 declarations
- RegularActions.lean 32 declarations
- RegularSplitting.lean 9 declarations
- RegularTorus.lean 41 declarations
- RelativeTrace.lean 5 declarations
- RepProducts.lean 8 declarations
- RepresentationMaps.lean 30 declarations
- RestrictedLift.lean 13 declarations
- RestrictedTarget.lean 21 declarations
- RestrictedTilting.lean 2 declarations
- SL2Definitions.lean 20 declarations
- SimpleModules.lean 33 declarations
- SmallGroupTrace.lean 19 declarations
- SpecializeCompletion.lean 7 declarations
- SplitRepresentation.lean 7 declarations
- StableKernel.lean 2 declarations
- StableRestriction.lean 5 declarations
- StandardLifts.lean 26 declarations
- SteinbergDuality.lean 13 declarations
- SteinbergRegular.lean 13 declarations
- SteinbergSpan.lean 8 declarations
- TensorAssociatedAction.lean 2 declarations
- TensorAssociatedIso.lean 3 declarations
- TensorCoordinates.lean 4 declarations
- TensorExactness.lean 10 declarations
- TensorFormalComparison.lean 2 declarations
- TensorLimits.lean 8 declarations
- TensorNumerator.lean 7 declarations
- TensorPlaneTilting.lean 3 declarations
- TensorWeights.lean 1 declarations
- ThetaTarget.lean 34 declarations
- TiltingBounds.lean 26 declarations
- TiltingCovers.lean 5 declarations
- TorusExtension.lean 4 declarations
- TorusRelations.lean 3 declarations
- TorusWeightProjection.lean 6 declarations
- TraceFactor.lean 9 declarations
- UnitAnnihilator.lean 6 declarations
- UnitSimple.lean 1 declarations
- WeightBounds.lean 25 declarations
- XChartLineEval.lean 11 declarations