OAI/GroupTheory/PolycyclicRecognition/Lattices/
331 declarations, 0 contain sorry, 0 declared as axioms; 101 files
Files
- AbelianCyclicFiniteIndexLattice.lean 2 declarations
- AbelianCyclicLattice.lean 2 declarations
- AbelianCyclicLogarithmLattice.lean 1 declarations
- AbelianLatticeKernel.lean 1 declarations
- AbelianLatticeRealization.lean 2 declarations
- BilinearCentralLattice.lean 3 declarations
- CartanNilshadow.lean 7 declarations
- CompletedExtensionCentralizer.lean 2 declarations
- CyclicCompletionHomUniqueness.lean 1 declarations
- DerivationSolvableModel.lean 5 declarations
- ExtensionFixedCocycleSection.lean 1 declarations
- FiniteFixedCocycleSection.lean 2 declarations
- FreeAbelianCyclicLattice.lean 4 declarations
- IntegerCyclicHomExtension.lean 1 declarations
- IntegerSemidirectLattice.lean 9 declarations
- IntegerTimeLattice.lean 4 declarations
- IntegralBilinearLattice.lean 6 declarations
- IntegralLatticeGenerators.lean 9 declarations
- IntegralLatticePowerIndex.lean 9 declarations
- IntegralNilshadow.lean 11 declarations
- JointFixedActionFiltration.lean 2 declarations
- JointFixedFactorSystem.lean 5 declarations
- JointFixedLayerAction.lean 5 declarations
- JointFixedReductionData.lean 9 declarations
- JointFixedResidualNilpotent.lean 1 declarations
- JointFixedSubalgebra.lean 7 declarations
- KernelCompletionAction.lean 8 declarations
- KernelCompletionCyclicHom.lean 1 declarations
- KernelCompletionCyclicStep.lean 2 declarations
- KernelCompletionEmbedding.lean 3 declarations
- KernelCompletionHeight.lean 7 declarations
- KernelCompletionTransport.lean 3 declarations
- KernelCompletionUnipotentLift.lean 1 declarations
- LatticeAutomorphismFlow.lean 1 declarations
- LatticeAutomorphismUnipotent.lean 1 declarations
- LatticeCharacterGeometry.lean 4 declarations
- LatticeCharacterSeparation.lean 1 declarations
- LatticeCharacterization.lean 2 declarations
- LatticeKernelTail.lean 4 declarations
- LatticeMetricChains.lean 2 declarations
- LatticeNormalFlag.lean 8 declarations
- LatticeQuotientDimension.lean 1 declarations
- LatticeRealizationFiniteIndex.lean 2 declarations
- LatticeTopLine.lean 3 declarations
- LatticeWordExtension.lean 6 declarations
- NilpotentCyclicFiniteIndexLattice.lean 1 declarations
- NilpotentCyclicHomExtension.lean 1 declarations
- NilpotentCyclicKernelCompletion.lean 2 declarations
- NilpotentCyclicLatticeExtension.lean 1 declarations
- NilpotentExtensionFixedFreeRealization.lean 1 declarations
- NilpotentExtensionLattice.lean 6 declarations
- NilpotentFiniteIndexLattice.lean 3 declarations
- NilpotentIntegralKernelCompletion.lean 2 declarations
- NilpotentKernelCompletion.lean 4 declarations
- NilpotentLatticeAbelianExtension.lean 1 declarations
- NilpotentLatticeAutomorphisms.lean 11 declarations
- NilpotentLatticeCoordinates.lean 3 declarations
- NilpotentLatticeCyclicExtension.lean 1 declarations
- NilpotentLatticeDerivationExtension.lean 1 declarations
- NilpotentLatticeDerivationLog.lean 2 declarations
- NilpotentLatticeInduction.lean 5 declarations
- NilpotentLatticeInnerAction.lean 4 declarations
- NilpotentLatticeInnerAdjoint.lean 2 declarations
- NilpotentLatticeInnerLogarithm.lean 1 declarations
- NilpotentLatticeLinearAction.lean 5 declarations
- NilpotentLatticeSemisimpleAction.lean 1 declarations
- NilpotentLatticeVectorAction.lean 1 declarations
- NilshadowGraphCover.lean 1 declarations
- NilshadowGraphTopology.lean 1 declarations
- NilshadowHeight.lean 15 declarations
- NilshadowLatticeRealization.lean 1 declarations
- NilshadowPowerGraph.lean 8 declarations
- NilshadowRealAction.lean 1 declarations
- NilshadowWeightAction.lean 11 declarations
- OrderedCyclicLatticeExtension.lean 1 declarations
- OriginalLatticeComparison.lean 1 declarations
- PolycyclicLatticeRealization.lean 3 declarations
- PolynomialLatticeExtension.lean 4 declarations
- RealActionIntegerLattice.lean 3 declarations
- RecognitionLatticeAssembly.lean 5 declarations
- SemidirectLatticeEmbedding.lean 2 declarations
- SemidirectUniformLattice.lean 3 declarations
- SemisimpleCentralizerCorrection.lean 1 declarations
- SemisimpleLangDecomposition.lean 2 declarations
- SmoothIntegralLatticeRealization.lean 1 declarations
- SmoothRealActionLattice.lean 1 declarations
- SmoothVectorActionLattice.lean 1 declarations
- SolvableLatticeModel.lean 3 declarations
- SolvableLatticePolycyclic.lean 2 declarations
- SolvableLatticeRecognition.lean 3 declarations
- TriangulableLatticePolycyclic.lean 1 declarations
- TwoStepFiniteIndexRealization.lean 2 declarations
- TwoStepLatticeRealization.lean 1 declarations
- UniformLatticeEmbedding.lean 2 declarations
- UniformLatticeFiniteGeneration.lean 2 declarations
- UniformLatticeFiniteIndexEmbedding.lean 2 declarations
- UniformLatticeMetric.lean 5 declarations
- UniformLatticeQuotient.lean 3 declarations
- UniformLatticeTransport.lean 2 declarations
- UniformLatticeWordMetric.lean 2 declarations
- VectorLatticeModel.lean 5 declarations