OAI/GroupTheory/PolycyclicRecognition/Algebra/

Files

• Abelian.lean 3 declarations
• AbelianByFiniteContractor.lean 3 declarations
• AbelianCyclicFiniteDimension.lean 2 declarations
• AbelianCyclicKernelRank.lean 7 declarations
• AbelianCyclicPolynomialNilpotence.lean 3 declarations
• AbelianCyclicSquareLog.lean 1 declarations
• AbelianCyclicTorsion.lean 3 declarations
• AbelianCyclicUnipotentNilpotence.lean 2 declarations
• AbelianDynkinInput.lean 6 declarations
• AbelianH2CrossProduct.lean 8 declarations
• AbelianH2ExteriorProduct.lean 5 declarations
• AbelianKernelPolynomialNilpotence.lean 1 declarations
• AbelianMultilinearNaturality.lean 2 declarations
• AbelianNormalExteriorInjection.lean 2 declarations
• AbelianNormalFieldRank.lean 2 declarations
• AbelianNormalFiniteDimension.lean 1 declarations
• AbelianNormalFiniteRank.lean 2 declarations
• AbelianNormalLargePrimeRank.lean 2 declarations
• AbelianNormalTorsion.lean 4 declarations
• AbelianPolynomialCoordinates.lean 1 declarations
• AbelianQuotientDimension.lean 1 declarations
• AbelianQuotientFiniteDimension.lean 1 declarations
• AbelianRankDimension.lean 3 declarations
• AbelianRealSpace.lean 11 declarations
• AbelianSubgroupRank.lean 4 declarations
• ActionDepth.lean 11 declarations
• ActionWordFiltration.lean 6 declarations
• ActiveRayConstraints.lean 6 declarations
• AdmissibleConjugateScheme.lean 5 declarations
• AdmissibleGeneratorWords.lean 6 declarations
• AdmissibleWordOperations.lean 5 declarations
• AlgebraGroupTangent.lean 8 declarations
• AlgebraOneParameter.lean 2 declarations
• AlgebraTangentSolvable.lean 1 declarations
• AlgebraicConjugationCharacters.lean 1 declarations
• AlgebraicDegreeOverTranscendentalField.lean 2 declarations
• AlgebraicExpandingEmbedding.lean 1 declarations
• AlgebraicIndependentPrimeQuotient.lean 1 declarations
• AlternatingBarCycles.lean 3 declarations
• AlternatingBarEvaluation.lean 5 declarations
• AlternatingBarFaces.lean 2 declarations
• AlternatingBarPermutation.lean 3 declarations
• AlternatingPolynomialCoordinates.lean 6 declarations
• AlternatingProductImage.lean 1 declarations
• AlternatingProductSubmersion.lean 6 declarations
• AlternatingTupleCoordinates.lean 2 declarations
• AlternatingWordOrder.lean 11 declarations
• AmbientSemisimpleCocycleReduction.lean 1 declarations
• AmplitudeWordCoordinates.lean 3 declarations
• AmplitudeWordImage.lean 1 declarations
• AmplitudeWordRank.lean 2 declarations
• ApproximateMidpointProper.lean 3 declarations
• AscendingBaseCoordinates.lean 3 declarations
• AscendingBaseLifting.lean 3 declarations
• AscendingCoinvariantRelations.lean 5 declarations
• AscendingExtensionDimension.lean 2 declarations
• AscendingNilpotentUnion.lean 1 declarations
• AscendingQuotientColimit.lean 4 declarations
• AscendingRefinement.lean 6 declarations
• AutocorrelationLowerBound.lean 2 declarations
• AutocorrelationRecurrence.lean 6 declarations
• AutomorphismCoinvariants.lean 4 declarations
• AutomorphismExhaustion.lean 11 declarations
• BackwardRecurrenceFamily.lean 2 declarations
• BackwardRecurrenceSets.lean 1 declarations
• BackwardRecurrenceStep.lean 4 declarations
• BarAutomorphism.lean 5 declarations
• BarCoefficientNaturality.lean 6 declarations
• BasepointLabelStabilization.lean 2 declarations
• BasisPolynomialMaps.lean 7 declarations
• BasisQuotientLifts.lean 5 declarations
• BilateralDifference.lean 14 declarations
• BilinearCentralGroup.lean 11 declarations
• BilinearGeneratorOrbit.lean 7 declarations
• BooleanPartitionMaps.lean 12 declarations
• BooleanStepAction.lean 3 declarations
• BooleanStepRing.lean 11 declarations
• BoundedCentralLayerSolvability.lean 1 declarations
• BoundedGeneratorSchemes.lean 4 declarations
• BoundedInverseCoding.lean 1 declarations
• BoundedLocallyFiniteKernel.lean 7 declarations
• BoundedPrefixEnvelope.lean 2 declarations
• BoundedSolvableRadical.lean 2 declarations
• BoundedWordAlgebra.lean 5 declarations
• BracketWords.lean 11 declarations
• BundleParameterCharts.lean 9 declarations
• BundleWordCoordinates.lean 5 declarations
• BundleWordImage.lean 1 declarations
• BundleWordRank.lean 2 declarations
• BundledCentralAverage.lean 1 declarations
• CanonicalNilpotentLogarithm.lean 6 declarations
• CayleyCaccioppoli.lean 1 declarations
• CayleyDirichletEnergy.lean 8 declarations
• CayleyWordLength.lean 6 declarations
• CayleyWordMaps.lean 3 declarations
• CenteredSourceTerminals.lean 3 declarations
• CentralBarLift.lean 8 declarations
• CentralBarProjection.lean 3 declarations
• CentralCocycleAverage.lean 2 declarations
• CentralCocycleSplitting.lean 14 declarations
• CentralCommutatorPowers.lean 4 declarations
• CentralCoordinateHom.lean 1 declarations
• CentralCoordinateQuotient.lean 3 declarations
• CentralDerivedTransgression.lean 2 declarations
• CentralExtensionTransgression.lean 7 declarations
• CentralExtensionTransgressionExact.lean 7 declarations
• CentralExtensionTransgressionKernel.lean 5 declarations
• CentralFiltrationAction.lean 3 declarations
• CentralJoinLowerCentral.lean 3 declarations
• CentralLayerAscendingBase.lean 2 declarations
• CentralLayerPairing.lean 5 declarations
• CentralLayerTensor.lean 10 declarations
• CentralLayerUnipotence.lean 3 declarations
• CentralLayersWordProjection.lean 1 declarations
• CentralTransgressionNaturality.lean 3 declarations
• CentralTransgressionRepresentation.lean 2 declarations
• CentralTransgressionSectionIndependence.lean 3 declarations
• CentralWordCollection.lean 2 declarations
• CentralizeContractor.lean 5 declarations
• CentralizerExtensionSplitting.lean 6 declarations
• ChamberBase.lean 8 declarations
• ChamberExtremeDirections.lean 5 declarations
• CharacterHemisphereEndgame.lean 1 declarations
• CharacterScaling.lean 3 declarations
• CharacterTamenessEndgame.lean 2 declarations
• CharacteristicCentralTransgression.lean 6 declarations
• CharacteristicCyclicSubgroup.lean 4 declarations
• CharacteristicFiniteIndex.lean 5 declarations
• CharacteristicKernelQuotient.lean 1 declarations
• CharacteristicQuotientAction.lean 3 declarations
• ChartedInvariantFrame.lean 5 declarations
• ChartedVectorFieldBracket.lean 8 declarations
• ChooseFaithfulMatrixRepresentation.lean 1 declarations
• ClassTwoCommutatorPairing.lean 9 declarations
• ClassTwoExteriorBracket.lean 9 declarations
• ClassTwoFiniteDimension.lean 2 declarations
• ClassTwoScalarBracket.lean 7 declarations
• ClosedEmbeddingSplitKernel.lean 2 declarations
• ClosedIntegrationOverLinearQuotient.lean 1 declarations
• ClosedNilpotentLinearKernel.lean 1 declarations
• CocycleCombing.lean 6 declarations
• CocycleGrowth.lean 9 declarations
• CoefficientConnectingNaturality.lean 5 declarations
• CofiberConnecting.lean 2 declarations
• CokernelHomModule.lean 2 declarations
• CollinearDynkin.lean 4 declarations
• CommonCentralizerSurjection.lean 1 declarations
• CommonDynkinFormula.lean 2 declarations
• CommonEigencharacterTorsion.lean 3 declarations
• CommonEigenspaceCommutators.lean 2 declarations
• CommonEigenvectors.lean 5 declarations
• CommonSemisimpleCentralizer.lean 5 declarations
• CommutingAscendingBases.lean 8 declarations
• CommutingDerivationAction.lean 10 declarations
• CommutingNilpotentWords.lean 2 declarations
• CommutingSemisimpleCorrection.lean 2 declarations
• CommutingSemisimpleFixedRepresentative.lean 1 declarations
• CommutingSubgroupProduct.lean 3 declarations
• CommutingUnipotentLogarithm.lean 2 declarations
• CompatiblePrimitives.lean 1 declarations
• CompleteValuedExtensions.lean 2 declarations
• ComplexBinaryWords.lean 5 declarations
• ComplexCharacterLift.lean 3 declarations
• ComplexDerivationDescent.lean 4 declarations
• ComplexFactorLocalChart.lean 9 declarations
• ComplexFactorParameters.lean 7 declarations
• ComplexMatrixExtension.lean 5 declarations
• ComplexSquareLogarithm.lean 3 declarations
• ComplexificationRealForm.lean 16 declarations
• ConditionalGroupRecognition.lean 2 declarations
• ConditionalKernelAlmostEverywhere.lean 1 declarations
• ConditionalKernelConsistency.lean 2 declarations
• ConditionalKernelFiber.lean 1 declarations
• ConditionalRecognition.lean 1 declarations
• ConeAdaptedMaximalBasis.lean 2 declarations
• ConeFacetTemplate.lean 2 declarations
• ConeIdealBasisExchange.lean 3 declarations
• ConeIdealGroup.lean 2 declarations
• ConeIdealGroupConjugation.lean 3 declarations
• ConeIdealInnerAutomorphism.lean 7 declarations
• ConeIdealStrictWidth.lean 4 declarations
• ConePolarTemplate.lean 11 declarations
• ConeQuotientAutomorphism.lean 4 declarations
• ConeQuotientBounds.lean 3 declarations
• ConeQuotientJacobian.lean 7 declarations
• ConeQuotientRestriction.lean 2 declarations
• ConeSectionBasis.lean 1 declarations
• ConeTraceSeparation.lean 2 declarations
• ConjugateCharacterLog.lean 4 declarations
• ConjugateEigenlineFreePair.lean 5 declarations
• ConjugateWindowStabilization.lean 8 declarations
• ConjugationDualSpectrum.lean 3 declarations
• ConjugationLift.lean 4 declarations
• ConnectedIdealNormality.lean 2 declarations
• ConnectedScalarCommutators.lean 4 declarations
• ConnectedSolvableEigenvector.lean 2 declarations
• ConnectedSolvableNilpotentDerived.lean 3 declarations
• ConnectedSolvableUnipotence.lean 1 declarations
• ConstructRiemannianInput.lean 1 declarations
• ConstructedNilpotentInputs.lean 4 declarations
• ConstructedNilpotentPublishedInputs.lean 1 declarations
• ContinuousOneParameter.lean 4 declarations
• ControlledCycleFillings.lean 7 declarations
• ControlledEquivariantMaps.lean 2 declarations
• ControlledGroupRingCoefficients.lean 6 declarations
• ControlledPrism.lean 5 declarations
• ControlledPrismEquation.lean 2 declarations
• ControlledPrismIdentity.lean 6 declarations
• ControlledProductPairs.lean 2 declarations
• ControlledReiterCocycles.lean 2 declarations
• CoordinateBilinearExpansion.lean 3 declarations
• CoordinateBoundedInverse.lean 2 declarations
• CoordinateConjugation.lean 4 declarations
• CoordinateConjugationDecay.lean 1 declarations
• CoordinateHomLinear.lean 2 declarations
• CoordinateInverseSections.lean 1 declarations
• CoordinateMatrixRepresentation.lean 7 declarations
• CoordinateMesh.lean 1 declarations
• CoordinateMinorPermutation.lean 9 declarations
• CoordinateOrbitRepresentation.lean 8 declarations
• CoordinatePolynomial.lean 4 declarations
• CoordinateSchemeBasis.lean 4 declarations
• CoordinateSchemeSubmersion.lean 3 declarations
• CoordinateWeakLinearity.lean 1 declarations
• CornulierTesseraConstruction.lean 1 declarations
• CountableFieldEmbeddings.lean 6 declarations
• CountableFreeRetract.lean 2 declarations
• CountableInvariantRepresentative.lean 2 declarations
• CountableSumPrefixes.lean 7 declarations
• CountableUnionDimension.lean 4 declarations
• CoupledBundleStates.lean 8 declarations
• CouplingLocalL2.lean 2 declarations
• CouplingTransfer.lean 12 declarations
• CyclicCoinvariants.lean 1 declarations
• CyclicConjugateGeneration.lean 6 declarations
• CyclicExteriorFiniteRank.lean 3 declarations
• CyclicExteriorOrbitDependence.lean 6 declarations
• CyclicJoinDimension.lean 5 declarations
• CyclicKernelGrowth.lean 2 declarations
• CyclicKernelPolynomialGrowth.lean 3 declarations
• CyclicKernelSplitting.lean 5 declarations
• CyclicParameterBasis.lean 4 declarations
• CyclicPingPong.lean 2 declarations
• CyclicPowerIndex.lean 8 declarations
• CyclicQuotientDimension.lean 2 declarations
• CyclicQuotientSequence.lean 6 declarations
• CyclicRegularExteriorObstruction.lean 13 declarations
• CyclicSchreierKernel.lean 6 declarations
• CyclicSquareIndex.lean 8 declarations
• DensityOccupationError.lean 2 declarations
• DensityTranslationLimits.lean 1 declarations
• DerivationEigenvectors.lean 3 declarations
• DeterminantLowerNorm.lean 3 declarations
• DiagonalDominantElement.lean 4 declarations
• DifferenceAmplitudeWord.lean 9 declarations
• DifferenceWordImage.lean 2 declarations
• DirectedDerivedSeries.lean 3 declarations
• DirectedLowerCentral.lean 4 declarations
• DiscreteLinearNilpotentKernel.lean 2 declarations
• DiscreteUnipotentAbelian.lean 2 declarations
• DiscreteUnipotentGroup.lean 1 declarations
• DistortedHomomorphisms.lean 3 declarations
• DixmierRegularityFromTopology.lean 2 declarations
• DominatedWordPrefixes.lean 1 declarations
• DualUnipotentPower.lean 5 declarations
• DynkinFiniteDifference.lean 6 declarations
• DynkinInput.lean 2 declarations
• DynkinIntegration.lean 5 declarations
• DynkinJacobian.lean 4 declarations
• DynkinLocalParameters.lean 6 declarations
• DynkinProductTails.lean 8 declarations
• DynkinSummableProducts.lean 3 declarations
• DynkinTranslationHomeomorph.lean 5 declarations
• DynkinTranslations.lean 3 declarations
• DynkinWords.lean 7 declarations
• EigenlineConeEstimates.lean 3 declarations
• EigenlineCones.lean 5 declarations
• EigenlinePingPong.lean 1 declarations
• EndomorphismCommutatorFiltration.lean 3 declarations
• EndomorphismInvariantFiniteIndex.lean 3 declarations
• EnvelopingDerivation.lean 12 declarations
• EnvelopingTruncation.lean 5 declarations
• EquivariantCentralizerSplitting.lean 2 declarations
• EquivariantCocycleReduction.lean 1 declarations
• EquivariantCommutatorFiltration.lean 3 declarations
• EquivariantLangTransversal.lean 3 declarations
• EventualPingPong.lean 1 declarations
• ExactTensorCoefficient.lean 3 declarations
• ExhaustionFunctionGluing.lean 1 declarations
• ExhaustionIndexBound.lean 1 declarations
• ExhaustionOrientation.lean 2 declarations
• ExhaustionOrientationDetection.lean 1 declarations
• ExhaustiveCharacter.lean 4 declarations
• ExpandedSchemeAmplitudes.lean 6 declarations
• ExpandingConjugationWords.lean 6 declarations
• ExpandingLinearRepresentation.lean 3 declarations
• ExtensionCentralizerKernel.lean 1 declarations
• ExtensionSectionFactor.lean 9 declarations
• ExtensionSemisimpleCentralizer.lean 5 declarations
• Extensions.lean 2 declarations
• ExteriorScalarDifference.lean 9 declarations
• ExteriorSquarePairing.lean 8 declarations
• ExteriorSquareRepresentation.lean 2 declarations
• ExtremeDirectionLabels.lean 3 declarations
• ExtremeTemplateLabels.lean 1 declarations
• FacetPivotBridgeRate.lean 2 declarations
• FacetReflectionTemplates.lean 3 declarations
• FactorAutomorphismDescent.lean 12 declarations
• FactorBridgeComposition.lean 4 declarations
• FactorExtensionConjugation.lean 3 declarations
• FactorExtensionMap.lean 3 declarations
• FactorExtensionTopology.lean 9 declarations
• FactorOccupationLimit.lean 1 declarations
• FactorOverlap.lean 1 declarations
• FactorQuotientAction.lean 3 declarations
• FactorQuotientIncrementBounds.lean 1 declarations
• FactorSystemCocycleReduction.lean 2 declarations
• FactorSystemGauge.lean 2 declarations
• FactorSystemPullback.lean 8 declarations
• FactorSystemSymmetry.lean 1 declarations
• FactorSystemSymmetrySubgroup.lean 1 declarations
• FactorSystemTwist.lean 5 declarations
• FactorSystemTwistAction.lean 4 declarations
• FactorTrajectoryIncrements.lean 1 declarations
• FaithfulGroupDynkin.lean 1 declarations
• FaithfulTruncatedEnveloping.lean 2 declarations
• FiberAverageL2.lean 10 declarations
• FiberIncrementBound.lean 4 declarations
• FieldCyclicKernelRank.lean 5 declarations
• FilteredBijection.lean 8 declarations
• FilteredDeterminant.lean 3 declarations
• FilteredNilpotentPerturbation.lean 2 declarations
• FilteredPolynomialPerturbation.lean 5 declarations
• FiniteAlgebraIndependentBound.lean 1 declarations
• FiniteAlgebraicConstants.lean 3 declarations
• FiniteBracketWords.lean 7 declarations
• FiniteCase.lean 2 declarations
• FiniteCentralLayerAction.lean 3 declarations
• FiniteCentralizerCommutator.lean 4 declarations
• FiniteCoefficientField.lean 4 declarations
• FiniteCofiber.lean 5 declarations
• FiniteCommutingOperatorAlgebra.lean 5 declarations
• FiniteConjugationIndexBound.lean 1 declarations
• FiniteCutoffPartition.lean 7 declarations
• FiniteCyclicOrbit.lean 3 declarations
• FiniteDimensionTorsionFree.lean 2 declarations
• FiniteDynkinDifference.lean 2 declarations
• FiniteExponentLinearGroups.lean 3 declarations
• FiniteExponentSubquotients.lean 2 declarations
• FiniteFiberMass.lean 1 declarations
• FiniteFinsuppHom.lean 5 declarations
• FiniteFrameDifferentiation.lean 2 declarations
• FiniteGeneratedCharacterLog.lean 2 declarations
• FiniteGraphCaccioppoli.lean 4 declarations
• FiniteGroupRationalTelescope.lean 13 declarations
• FiniteGroupRelativeInjective.lean 7 declarations
• FiniteIndexKernelQuotient.lean 3 declarations
• FiniteIndexNormalExtension.lean 1 declarations
• FiniteIndexOrientation.lean 2 declarations
• FiniteIndexRestriction.lean 4 declarations
• FiniteIndexTrace.lean 4 declarations
• FiniteIndexTraceRetract.lean 15 declarations
• FiniteInduction.lean 4 declarations
• FiniteIntegerReductions.lean 5 declarations
• FiniteInvariantOrbit.lean 5 declarations
• FiniteKernelAbelianQuotient.lean 1 declarations
• FiniteKernelAscendingBase.lean 7 declarations
• FiniteKernelAscendingData.lean 2 declarations
• FiniteKernelSolvable.lean 3 declarations
• FiniteKernelSubgroupBounds.lean 3 declarations
• FiniteLabelReflection.lean 2 declarations
• FiniteLinearSymmetries.lean 2 declarations
• FiniteLogCoefficientBound.lean 3 declarations
• FiniteModuleIndependentBound.lean 1 declarations
• FiniteNormalGeneration.lean 4 declarations
• FiniteNormalRadical.lean 2 declarations
• FiniteOrbitAscendingBase.lean 6 declarations
• FiniteOrbitAverage.lean 8 declarations
• FiniteOrbitContractor.lean 7 declarations
• FiniteOrderAscendingBase.lean 2 declarations
• FiniteOrderMatrixTraces.lean 4 declarations
• FiniteOrderUnipotent.lean 1 declarations
• FiniteProductGlobalChart.lean 1 declarations
• FiniteProductPolynomialCoordinates.lean 2 declarations
• FiniteRationalLinearModel.lean 2 declarations
• FiniteRationalRepresentation.lean 7 declarations
• FiniteRepresentationQuotients.lean 2 declarations
• FiniteRestriction.lean 3 declarations
• FiniteSemisimpleCocycleReduction.lean 1 declarations
• FiniteSemisimpleLiftFamily.lean 4 declarations
• FiniteShiftProductAlgebra.lean 7 declarations
• FiniteSignOrder.lean 2 declarations
• FiniteSolvableDerivedBound.lean 4 declarations
• FiniteSwitchEvents.lean 4 declarations
• FiniteTopOrientation.lean 1 declarations
• FiniteTorsionPowerSubgroup.lean 5 declarations
• FiniteTraceLinearGroup.lean 1 declarations
• FiniteTypeExpandingEmbedding.lean 2 declarations
• FiniteTypeTorsionEigenvalues.lean 2 declarations
• FiniteTypeTorsionLinearGroups.lean 1 declarations
• FiniteUnitaryAverage.lean 10 declarations
• FiniteWordBases.lean 7 declarations
• FinitelyGeneratedCountable.lean 1 declarations
• FinitelyGeneratedLift.lean 2 declarations
• FinsuppRepresentationModule.lean 1 declarations
• FixedChartTranslation.lean 2 declarations
• FixedLogQuotient.lean 3 declarations
• FixedPowerLogarithms.lean 2 declarations
• FreeAbelianCentralExtension.lean 1 declarations
• FreeAbelianLogarithm.lean 4 declarations
• FreeCoefficientCoinvariants.lean 2 declarations
• GaugeComposition.lean 2 declarations
• GaugeExtensionSection.lean 3 declarations
• GaugeFactorSymmetry.lean 1 declarations
• GeneratedUnipotentAction.lean 2 declarations
• GeneratorConjugation.lean 7 declarations
• GeneratorOrbit.lean 14 declarations
• GeneratorSchemes.lean 7 declarations
• GeneratorWordPadding.lean 4 declarations
• GenericJointChambers.lean 1 declarations
• GeodesicWords.lean 1 declarations
• GlobalGeneratorWords.lean 2 declarations
• GoodFiniteWordVertices.lean 7 declarations
• GoodSheetWordImage.lean 1 declarations
• GoodSourceBundleImage.lean 1 declarations
• GradedCoordinateLimit.lean 5 declarations
• GradedGeneratorLimit.lean 6 declarations
• GradedHorizontalStructure.lean 5 declarations
• GromovGrowthBridge.lean 3 declarations
• GromovInput.lean 5 declarations
• GromovLinearReduction.lean 4 declarations
• GroupAveragedRepresentative.lean 6 declarations
• GroupCocycleCoboundary.lean 3 declarations
• GroupExtensionFactorSystem.lean 7 declarations
• GroupFiniteGenerationFromFP.lean 10 declarations
• GroupLikeNilpotentLogarithm.lean 1 declarations
• GroupedGoodWords.lean 5 declarations
• GrowingPositiveParameters.lean 1 declarations
• HigherExteriorFiniteRank.lean 2 declarations
• HigherExteriorFreeOrbitBound.lean 1 declarations
• HilbertOrbitAverage.lean 7 declarations
• HomeomorphicParameter.lean 2 declarations
• HomogeneousGenerators.lean 5 declarations
• HomogeneousUniversalLogarithm.lean 8 declarations
• HomogeneousWordCoefficients.lean 6 declarations
• HomogeneousWordProjection.lean 7 declarations
• HorizontalExtremeSpanning.lean 1 declarations
• HorizontalGeneratorChange.lean 1 declarations
• HyperplaneReflection.lean 2 declarations
• IdealProductCoordinates.lean 2 declarations
• ImaginaryOperatorPolynomial.lean 3 declarations
• IncreasingUnionDimension.lean 1 declarations
• IndependentAlgebraicConstants.lean 2 declarations
• IndependentSwitchParameters.lean 8 declarations
• InducedBarTranslation.lean 4 declarations
• InducedCyclicDifference.lean 5 declarations
• InducedTranslation.lean 5 declarations
• InductionAmbientQuotient.lean 6 declarations
• InductionSemilinear.lean 4 declarations
• InductionTrivial.lean 4 declarations
• InfiniteAbelianIntegerQuotient.lean 1 declarations
• InfiniteCyclicDifference.lean 2 declarations
• InfiniteFieldExteriorRank.lean 2 declarations
• InnerBarTranslation.lean 7 declarations
• InnerCentralizerFactorSystem.lean 2 declarations
• InnerCentralizerMembership.lean 1 declarations
• InnerCentralizerProduct.lean 12 declarations
• IntegerConjugationUnipotent.lean 3 declarations
• IntegerExtensionRank.lean 2 declarations
• IntegerInducedTranslation.lean 5 declarations
• IntegerQuotientCoordinates.lean 10 declarations
• IntegerQuotientStructure.lean 5 declarations
• IntegerRegularCoordinates.lean 6 declarations
• IntegrationToUnipotentModel.lean 1 declarations
• IntertwinedActionWords.lean 3 declarations
• IntertwinedUnipotence.lean 3 declarations
• IntrinsicGroupDynkin.lean 1 declarations
• IntrinsicIdealNormality.lean 2 declarations
• InvariantDisintegration.lean 10 declarations
• InvariantFactor.lean 15 declarations
• InvariantFactorComponents.lean 2 declarations
• InvariantFactorObservables.lean 5 declarations
• InvariantL2Representative.lean 2 declarations
• InvariantLinearLayer.lean 4 declarations
• InvariantSubspaceDeterminant.lean 3 declarations
• InvariantTopTwist.lean 1 declarations
• InverseAverageL2.lean 5 declarations
• InverseCoupling.lean 1 declarations
• InverseDefectControl.lean 2 declarations
• InverseErrorBound.lean 2 declarations
• InverseSection.lean 3 declarations
• InverseTransferIdentity.lean 6 declarations
• InwardVectorCharacters.lean 6 declarations
• IrreducibleDominantFreePair.lean 3 declarations
• IrreducibleFiniteTrace.lean 2 declarations
• IrreducibleGenericConjugator.lean 2 declarations
• IteratedCoinvariants.lean 5 declarations
• JointDirectionLabels.lean 7 declarations
• KernelConullRepair.lean 1 declarations
• KernelLinearSplitting.lean 1 declarations
• KernelProductCoordinates.lean 1 declarations
• L2LabelDistance.lean 1 declarations
• LeftInvariantRiemannianDistance.lean 5 declarations
• LeftInvariantRiemannianLength.lean 5 declarations
• LeftTangentTrivialization.lean 7 declarations
• LinearActionFiltration.lean 7 declarations
• LinearCocycleReduction.lean 1 declarations
• LinearConjugationCentralizer.lean 3 declarations
• LinearInvariantInverse.lean 1 declarations
• LinearNilpotentKernel.lean 1 declarations
• LinearOrbitSpan.lean 2 declarations
• ListBarCoordinates.lean 6 declarations
• ListBarHomogeneous.lean 7 declarations
• ListBarInsertionHomotopy.lean 3 declarations
• ListBarPairHomotopy.lean 4 declarations
• ListBarProduct.lean 5 declarations
• ListBarProductPrism.lean 6 declarations
• ListBarShuffle.lean 14 declarations
• ListTupleUpdate.lean 2 declarations
• LocalCoordinateScheme.lean 1 declarations
• LocalGeneratorAccessibility.lean 2 declarations
• LocalGeneratorOrbit.lean 6 declarations
• LocalRiemannianChart.lean 1 declarations
• LocalSolvableRadical.lean 5 declarations
• LocalSubmersion.lean 1 declarations
• LocalVirtualSolvabilityBound.lean 4 declarations
• LocallyAlgebraicRepresentation.lean 3 declarations
• LocallyBoundedDerivedSeries.lean 7 declarations
• LocallyNilpotentDimension.lean 6 declarations
• LocallyNilpotentRationalEndgame.lean 2 declarations
• LocallyNilpotentTorsion.lean 8 declarations
• LogDistortion.lean 4 declarations
• LogPolynomialBounds.lean 1 declarations
• LogarithmCoefficientStability.lean 3 declarations
• LogarithmicCocycleWords.lean 3 declarations
• LowerCentralExhaustion.lean 1 declarations
• MappedBasisBrackets.lean 1 declarations
• MassFractionBounds.lean 3 declarations
• MaximalAbelianNormal.lean 2 declarations
• MaximalNilpotentCentralAction.lean 6 declarations
• MaximalNilpotentNormal.lean 2 declarations
• MaximizingCoordinateCriterion.lean 1 declarations
• MeasurableGeneratorPrefixes.lean 2 declarations
• MidpointGrids.lean 11 declarations
• MixedWordBasis.lean 7 declarations
• MixedWordIdeal.lean 10 declarations
• ModelDensityOccupation.lean 1 declarations
• MonicRecurrenceAscendingBase.lean 2 declarations
• MonoidCoefficientLinear.lean 5 declarations
• MonoidModuleAscendingBase.lean 4 declarations
• MonoidRingOrbitSpan.lean 5 declarations
• MonoidTensorCoordinates.lean 11 declarations
• MultilinearCoordinatePair.lean 3 declarations
• NatTotalComplexSymmetry.lean 1 declarations
• NegativeRayDescent.lean 8 declarations
• Nilpotent.lean 2 declarations
• NilpotentAbelianQuotientRank.lean 2 declarations
• NilpotentAbelianizationGenerators.lean 2 declarations
• NilpotentAbelianizedDimension.lean 2 declarations
• NilpotentAlgebraRepresentation.lean 1 declarations
• NilpotentAscendingBase.lean 3 declarations
• NilpotentAutomorphism.lean 5 declarations
• NilpotentAutomorphismAction.lean 1 declarations
• NilpotentAutomorphismDifference.lean 4 declarations
• NilpotentBasisWordChoices.lean 1 declarations
• NilpotentByAbelianRationalDimension.lean 2 declarations
• NilpotentByAbelianRealization.lean 1 declarations
• NilpotentByAbelianReduction.lean 2 declarations
• NilpotentByAbelianSplitRealization.lean 1 declarations
• NilpotentByCyclicRealization.lean 1 declarations
• NilpotentChartCountability.lean 1 declarations
• NilpotentClassBound.lean 5 declarations
• NilpotentCodimensionOne.lean 6 declarations
• NilpotentCodimensionOneCriterion.lean 3 declarations
• NilpotentCodimensionOneModel.lean 1 declarations
• NilpotentConjugationCoordinates.lean 1 declarations
• NilpotentConjugationDecay.lean 2 declarations
• NilpotentConjugationWords.lean 4 declarations
• NilpotentContinuousRepresentation.lean 1 declarations
• NilpotentContractorEndgame.lean 6 declarations
• NilpotentCoordinatesInput.lean 5 declarations
• NilpotentCyclicRealization.lean 1 declarations
• NilpotentExhaustionDimension.lean 3 declarations
• NilpotentExtensionEmbedding.lean 5 declarations
• NilpotentExtensionFactorSystem.lean 3 declarations
• NilpotentExtensionLangSplitting.lean 2 declarations
• NilpotentExtensionRealization.lean 1 declarations
• NilpotentFaithfulIntegration.lean 1 declarations
• NilpotentFaithfulRepresentation.lean 1 declarations
• NilpotentFiniteCentralizer.lean 1 declarations
• NilpotentFiniteTailBound.lean 3 declarations
• NilpotentGeneratorRank.lean 4 declarations
• NilpotentGenerators.lean 4 declarations
• NilpotentIdealDerivation.lean 5 declarations
• NilpotentIdealNorm.lean 1 declarations
• NilpotentIntegrationConstruction.lean 1 declarations
• NilpotentIntrinsicIntegration.lean 1 declarations
• NilpotentLangMap.lean 1 declarations
• NilpotentLogIntertwiner.lean 2 declarations
• NilpotentMatrixProducts.lean 1 declarations
• NilpotentMatrixSpanning.lean 2 declarations
• NilpotentModelConstruction.lean 7 imports, no declarations
• NilpotentModelIntegration.lean 1 declarations
• NilpotentPolyZ.lean 4 declarations
• NilpotentPolynomialConjugation.lean 1 declarations
• NilpotentPolynomialOperations.lean 2 declarations
• NilpotentPolynomialRepresentation.lean 2 declarations
• NilpotentPowerSeriesEvaluation.lean 4 declarations
• NilpotentPowerSeriesSubstitution.lean 3 declarations
• NilpotentProducts.lean 11 declarations
• NilpotentPublishedInputs.lean 6 declarations
• NilpotentQuotientIntegration.lean 1 declarations
• NilpotentQuotientRank.lean 4 declarations
• NilpotentRationalConjugation.lean 8 declarations
• NilpotentRecognition.lean 2 declarations
• NilpotentRepresentationProducts.lean 1 declarations
• NilpotentSectionRemainder.lean 6 declarations
• NilpotentSpanningOperators.lean 1 declarations
• NilpotentTorsionQuotientEndgame.lean 3 declarations
• NilpotentTorsionSubgroup.lean 11 declarations
• NilpotentUniversalLogarithm.lean 3 declarations
• NilpotentWordEvaluation.lean 7 declarations
• NoetherianComponents.lean 2 declarations
• NonabelianFactorSystem.lean 18 declarations
• NormalAbelianizationModule.lean 5 declarations
• NormalAbelianizationQuotient.lean 5 declarations
• NormalBarConjugation.lean 5 declarations
• NormalCentralQuotientAction.lean 8 declarations
• NormalCoinvariantsInflationIso.lean 4 declarations
• NormalCyclicTopStep.lean 1 declarations
• NormalEigencharacters.lean 7 declarations
• NormalInductionCoordinates.lean 10 declarations
• NormalInductionExact.lean 8 declarations
• NormalInductionTensor.lean 17 declarations
• NormalProductRepresentation.lean 1 declarations
• NormalQuotientCoordinates.lean 7 declarations
• NormalizePositiveMass.lean 1 declarations
• NormalizedFreeColimit.lean 22 declarations
• NormalizedFreeRepresentation.lean 15 declarations
• NormalizedGeneration.lean 2 declarations
• NormalizedGroupLaws.lean 4 declarations
• NormalizedIdentityClass.lean 6 declarations
• NormalizedIdentityConnecting.lean 2 declarations
• NormalizedIdentityScalar.lean 1 declarations
• NormalizedPairInverseLabels.lean 1 declarations
• NormalizedTupleDomain.lean 2 declarations
• NormalizedWordBrackets.lean 4 declarations
• NumberFieldExpandingPlace.lean 3 declarations
• NumberFieldTorsionLinearGroups.lean 1 declarations
• OccupationDomination.lean 3 declarations
• OccupationLimitSelection.lean 2 declarations
• OccupationMicrostepLimit.lean 1 declarations
• OccupationMicrosteps.lean 2 declarations
• OccupationTranslation.lean 2 declarations
• OccupationWeakLimit.lean 2 declarations
• OneSidedDominantDynamics.lean 3 declarations
• OneSidedOrbitAscendingBase.lean 5 declarations
• OpenProductRepresentation.lean 1 declarations
• OrbitAverageLimitMass.lean 2 declarations
• OrderedCentralWords.lean 7 declarations
• OrderedInterpolation.lean 10 declarations
• OrderedInterpolationRadius.lean 3 declarations
• OrderedPowerWords.lean 4 declarations
• OrderedProductSums.lean 1 declarations
• OrientationInnerAction.lean 3 declarations
• PairAction.lean 13 declarations
• PairApproximation.lean 3 declarations
• PairCharts.lean 14 declarations
• PairCoupling.lean 10 declarations
• PairLabelFunctions.lean 2 declarations
• PairMicrosteps.lean 4 declarations
• PairOrbit.lean 9 declarations
• PairedExhaustionIndex.lean 2 declarations
• PairedWordCoproduct.lean 4 declarations
• ParameterDensityMass.lean 2 declarations
• ParameterSplit.lean 1 declarations
• ParameterizedAdmissibleWords.lean 2 declarations
• ParametricInverseSection.lean 2 declarations
• ParametricSubmersion.lean 2 declarations
• ParametrizedGeneratorSchemes.lean 4 declarations
• PerturbedInversePairs.lean 1 declarations
• PiFiberMass.lean 4 declarations
• PointwiseAlgebraicEndomorphism.lean 2 declarations
• PointwiseOrbitAverages.lean 2 declarations
• PolyZ.lean 7 declarations
• PolyZComparison.lean 3 declarations
• PolyZExtension.lean 6 declarations
• PolyZFiniteIndex.lean 2 declarations
• PolyZNormalExtension.lean 5 declarations
• Polycyclic.lean 9 declarations
• PolycyclicExtensionDimension.lean 2 declarations
• PolycyclicFiniteGeneration.lean 4 declarations
• PolycyclicPolynomialNilpotence.lean 3 declarations
• PolycyclicQuotientRank.lean 3 declarations
• PolycyclicTorsionFree.lean 4 declarations
• PolyhedralSymmetries.lean 1 declarations
• PolynomialBilinearWords.lean 3 declarations
• PolynomialCentralLayerUnipotence.lean 2 declarations
• PolynomialChartCoordinates.lean 2 declarations
• PolynomialCoefficientContinuity.lean 3 declarations
• PolynomialCommutingProduct.lean 2 declarations
• PolynomialConjugationSpectrum.lean 3 declarations
• PolynomialCoordinateAction.lean 4 declarations
• PolynomialCoordinateCurves.lean 5 declarations
• PolynomialCoordinateEvaluation.lean 7 declarations
• PolynomialCoordinateGroup.lean 9 declarations
• PolynomialCoordinateIntegration.lean 6 declarations
• PolynomialCoordinateOperations.lean 10 declarations
• PolynomialCoordinateOrbit.lean 4 declarations
• PolynomialCoordinateTopology.lean 5 declarations
• PolynomialCoordinateWords.lean 5 declarations
• PolynomialCurveOperations.lean 4 declarations
• PolynomialDerivationAction.lean 4 declarations
• PolynomialDerivationCoordinates.lean 3 declarations
• PolynomialEnvelopes.lean 2 declarations
• PolynomialExteriorDeterminant.lean 9 declarations
• PolynomialExteriorShiftOperators.lean 6 declarations
• PolynomialFamilies.lean 12 declarations
• PolynomialFunctionSpace.lean 6 declarations
• PolynomialGroupDifference.lean 1 declarations
• PolynomialGroupLaws.lean 9 declarations
• PolynomialGroupNilpotence.lean 1 declarations
• PolynomialGrowth.lean 2 declarations
• PolynomialGrowthImages.lean 3 declarations
• PolynomialGrowthLinearImage.lean 2 declarations
• PolynomialGrowthNilpotentCentralLayers.lean 2 declarations
• PolynomialGrowthNoFreePair.lean 6 declarations
• PolynomialGrowthPingPong.lean 1 declarations
• PolynomialGrowthSemigroupPingPong.lean 4 declarations
• PolynomialGrowthSubgroups.lean 3 declarations
• PolynomialIdealCongruence.lean 4 declarations
• PolynomialIdealExtensionCoordinates.lean 1 declarations
• PolynomialInnerLogarithm.lean 4 declarations
• PolynomialInnerUnipotence.lean 4 declarations
• PolynomialIntegerGrid.lean 7 declarations
• PolynomialInterpolationBound.lean 2 declarations
• PolynomialLangTransversal.lean 1 declarations
• PolynomialLargeValueSet.lean 1 declarations
• PolynomialLowerCentralProjection.lean 2 declarations
• PolynomialMatrixCommutator.lean 5 declarations
• PolynomialMatrixFunctions.lean 14 declarations
• PolynomialMatrixGenericPosition.lean 2 declarations
• PolynomialMatrixGroup.lean 20 declarations
• PolynomialMatrixLogarithm.lean 1 declarations
• PolynomialMatrixRepresentation.lean 5 declarations
• PolynomialMatrixScalarExtension.lean 6 declarations
• PolynomialMatrixStabilizer.lean 9 declarations
• PolynomialMinor.lean 3 declarations
• PolynomialModelDifference.lean 4 declarations
• PolynomialModelDynkin.lean 2 declarations
• PolynomialModelHom.lean 4 declarations
• PolynomialModelRepresentation.lean 6 declarations
• PolynomialModelWords.lean 8 declarations
• PolynomialOneParameterNilpotent.lean 4 declarations
• PolynomialOneParameterUniqueness.lean 1 declarations
• PolynomialOperatorDetector.lean 3 declarations
• PolynomialOrbitExterior.lean 6 declarations
• PolynomialParameterExtension.lean 3 declarations
• PolynomialPrefixEnvelope.lean 1 declarations
• PolynomialProductParameters.lean 5 declarations
• PolynomialQuotientAction.lean 6 declarations
• PolynomialRangeAgreement.lean 2 declarations
• PolynomialRepresentationCurves.lean 3 declarations
• PolynomialSliceGrowth.lean 4 declarations
• PolynomialSubalgebraCoordinates.lean 5 declarations
• PolynomialSubalgebraFiltration.lean 3 declarations
• PolynomialSubalgebraGroup.lean 6 declarations
• PolynomialSubalgebraNilpotence.lean 5 declarations
• PolynomialTranslationLimits.lean 3 declarations
• PolynomialTripling.lean 3 declarations
• PolynomialUnipotentModel.lean 1 declarations
• PositiveAnnihilatorCriterion.lean 3 declarations
• PositiveAnnihilatorPropagation.lean 1 declarations
• PositiveCharacterIdeal.lean 8 declarations
• PositiveCharacterOrbitSpan.lean 7 declarations
• PositiveParameterSets.lean 1 declarations
• PositiveRayPullback.lean 1 declarations
• PositiveRescaling.lean 2 declarations
• PositiveVariationEquality.lean 1 declarations
• PositiveWidthAbsorption.lean 4 declarations
• PositiveWidthSmallLog.lean 1 declarations
• PositiveZeroSums.lean 2 declarations
• PowerDominantEigenlines.lean 3 declarations
• PowersModuleAscendingBase.lean 3 declarations
• PresentationKernelMap.lean 12 declarations
• PrimitiveWordProjection.lean 5 declarations
• ProductLocalCoordinates.lean 2 declarations
• ProjectedFactorSystem.lean 1 declarations
• PublishedRecognitionInputs.lean 14 declarations
• PullbackInnerProduct.lean 4 declarations
• PullbackTangentCoordinates.lean 2 declarations
• PullbackVectorFieldCoordinates.lean 1 declarations
• QuotientGroupAction.lean 5 declarations
• QuotientLinearAction.lean 2 declarations
• QuotientSectionCoordinates.lean 6 declarations
• QuotientSectionIndependence.lean 1 declarations
• QuotientTrace.lean 1 declarations
• QuotientWordBasis.lean 4 declarations
• RankOneCharacter.lean 5 declarations
• RankOneEndomorphisms.lean 1 declarations
• RankOneRepresentation.lean 5 declarations
• RationalAbelianRank.lean 7 declarations
• RationalAbelianTorsion.lean 3 declarations
• RationalCentralLayers.lean 6 declarations
• RationalCentralTransgression.lean 3 declarations
• RationalCharacterCancellation.lean 4 declarations
• RationalCoefficientSequence.lean 9 declarations
• RationalCompleteIdentity.lean 5 declarations
• RationalConjugation.lean 8 declarations
• RationalExtensionDimension.lean 2 declarations
• RationalFiniteCoinvariants.lean 7 declarations
• RationalFiniteQuotient.lean 12 declarations
• RationalGroupDimension.lean 3 declarations
• RationalInvariantTopClass.lean 2 declarations
• RationalLineProperties.lean 2 declarations
• RationalLocallyNilpotentDimension.lean 4 declarations
• RationalModuleFunctor.lean 6 declarations
• RationalNilpotentClassBound.lean 2 declarations
• RationalNilpotentQuotient.lean 8 declarations
• RationalNilpotentRank.lean 5 declarations
• RationalNilpotentTorsion.lean 3 declarations
• RationalNormalExtensionBound.lean 3 declarations
• RationalOrientationCoefficient.lean 5 declarations
• RationalOrientationConjugation.lean 2 declarations
• RationalOrientationExtension.lean 2 declarations
• RationalPowerSeriesHom.lean 4 declarations
• RationalRankOneAction.lean 5 declarations
• RationalRecognitionEndgame.lean 1 declarations
• RationalRepresentationFunctor.lean 15 declarations
• RationalScalarTwist.lean 5 declarations
• RationalSolvableDimension.lean 3 declarations
• RationalSpanDenominators.lean 1 declarations
• RationalSubgroupFiltration.lean 7 declarations
• RationalTensorDimension.lean 2 declarations
• RationalTensorNaturality.lean 2 declarations
• RationalTorsionEigenvalues.lean 2 declarations
• RationalTorsionLinearGroups.lean 2 declarations
• RationalUniversalLogarithm.lean 10 declarations
• RationalWordCoproduct.lean 5 declarations
• RationalWordEvaluation.lean 5 declarations
• RationalWordOperators.lean 6 declarations
• RationalWordTruncationEvaluation.lean 2 declarations
• RayBoundedRepresentatives.lean 2 declarations
• RayHalfspace.lean 2 declarations
• RayIdealConjugation.lean 2 declarations
• RayIdealTemplates.lean 3 declarations
• RayMixedWidths.lean 3 declarations
• RealEigenAnnihilator.lean 4 declarations
• RealEndComplexification.lean 5 declarations
• RealEndDescent.lean 5 declarations
• RealGramDeterminantOrder.lean 4 declarations
• RealGramLargeSubspace.lean 5 declarations
• RealGramSimultaneousDiagonal.lean 3 declarations
• RealMatrixSquareLogarithm.lean 3 declarations
• RealNilpotentLogIntertwiner.lean 2 declarations
• RealNilpotentSpanningOperators.lean 1 declarations
• RealParameterEquicontinuity.lean 2 declarations
• RealSemisimpleCommutingLogarithm.lean 1 declarations
• RealSemisimpleLogarithm.lean 4 declarations
• RealSplitAnnihilator.lean 1 declarations
• RealTorusAction.lean 7 declarations
• RealTorusContinuity.lean 4 declarations
• RecognitionFromLeafTraces.lean 1 declarations
• RecognitionFromPairRepresentatives.lean 1 declarations
• RecognitionFromPolycyclicComparison.lean 1 declarations
• RecognitionWithoutKMN.lean 5 declarations
• RectangleFiberMass.lean 1 declarations
• RecurrentSourceBundles.lean 1 declarations
• RecurrentWordImage.lean 1 declarations
• RegularCoefficientAction.lean 4 declarations
• RegularCoefficientNaturality.lean 5 declarations
• RegularDualFree.lean 7 declarations
• RegularDualPairing.lean 11 declarations
• RegularDualRepresentation.lean 8 declarations
• RegularEvaluationKernel.lean 3 declarations
• RegularFreeEvaluation.lean 5 declarations
• RegularHilbertRepresentation.lean 16 declarations
• RegularLazyWalk.lean 8 declarations
• RegularPairingNaturality.lean 3 declarations
• RegularWalkEnergyLowerBound.lean 3 declarations
• RelatedVectorFieldBracket.lean 1 declarations
• RelativeCommutatorSeries.lean 6 declarations
• RelativeNilpotentExtension.lean 2 declarations
• RelativeSemisimpleCorrection.lean 1 declarations
• RepCofiber.lean 16 declarations
• RepresentationDirectSum.lean 9 declarations
• RepresentationFiniteDescent.lean 2 declarations
• RepresentationFiniteRestriction.lean 1 declarations
• RepresentationKernelCoordinates.lean 1 declarations
• RepresentationOrbitGenerators.lean 2 declarations
• RepresentationParameterChart.lean 1 declarations
• RepresentationSumExact.lean 8 declarations
• RepresentedMatrixChoice.lean 1 declarations
• RescaledBasisChange.lean 2 declarations
• RescaledBasisMonotone.lean 2 declarations
• RescaledChartDistances.lean 2 declarations
• RescaledDensityOccupation.lean 1 declarations
• RescaledFixedTranslation.lean 1 declarations
• RescaledGeneratorBounds.lean 2 declarations
• RescaledInverseSections.lean 1 declarations
• RescaledPivotLegs.lean 1 declarations
• RescaledProductEnvelope.lean 1 declarations
• RescaledSubmersiveScheme.lean 3 declarations
• RescaledTwoImageLimit.lean 5 declarations
• RescaledUniformGeneration.lean 2 declarations
• RescaledWordPrefixes.lean 1 declarations
• RescaledWordSums.lean 2 declarations
• ResidualLowerCentralLayers.lean 9 declarations
• RestrictedRegular.lean 5 declarations
• RestrictionEquivalence.lean 2 declarations
• ReweightedFrameBracket.lean 1 declarations
• RiemannianApproximateMidpoints.lean 2 declarations
• RiemannianChartLength.lean 1 declarations
• RightTranslationInvariant.lean 2 declarations
• RightTranslationLabel.lean 4 declarations
• RingTraceProjectivity.lean 6 declarations
• ScalarAlternatingExtension.lean 5 declarations
• ScalarExtendedH2CrossProduct.lean 13 declarations
• ScalarExteriorSurjection.lean 4 declarations
• ScalarH2BilinearDetection.lean 6 declarations
• ScalarH2CrossProductNaturality.lean 2 declarations
• ScalarHigherExteriorDetection.lean 5 declarations
• ScalarHigherExteriorNaturality.lean 3 declarations
• ScalarHigherExteriorProduct.lean 4 declarations
• ScalarHigherProductNaturality.lean 1 declarations
• ScalarMultilinearExtension.lean 5 declarations
• SchurTorsionLinearGroups.lean 2 declarations
• SectionErrorAbsorption.lean 4 declarations
• SectionFactorTopology.lean 4 declarations
• SemisimpleCentralDecomposition.lean 4 declarations
• SemisimpleCentralizerExtension.lean 4 declarations
• SemisimpleCocycleReduction.lean 1 declarations
• SemisimpleCocycleReductionPreserving.lean 1 declarations
• SemisimpleInnerCentralizer.lean 3 declarations
• SemisimpleInnerFixedRepresentative.lean 2 declarations
• SemisimpleKernelProjection.lean 8 declarations
• SemisimpleLangTransversal.lean 1 declarations
• SemisimpleMovingAction.lean 7 declarations
• SemisimpleMovingLang.lean 4 declarations
• SemisimpleSpectralOperator.lean 6 declarations
• SemisimpleSquareLog.lean 2 declarations
• SeparateConnectedGeneration.lean 2 declarations
• SeparateDerivedClosure.lean 3 declarations
• SeparateFiniteIndexDensity.lean 2 declarations
• SeparateGroupClosure.lean 9 declarations
• SeparateIrreducibleComponent.lean 9 declarations
• SequenceBackwardRecurrence.lean 1 declarations
• SequenceDifferenceWordImage.lean 2 declarations
• SequenceFiniteSubexponential.lean 2 declarations
• SequenceParameterDensity.lean 1 declarations
• SequencePolynomialValues.lean 1 declarations
• SequencePositiveParameters.lean 1 declarations
• SequenceRealExtension.lean 6 declarations
• SequenceRecurrentWordImage.lean 1 declarations
• SequenceSubexponential.lean 11 declarations
• SequenceSubexponentialOperations.lean 8 declarations
• SequenceSubexponentialRate.lean 1 declarations
• SequenceSubsequences.lean 3 declarations
• SequenceSuccessfulParameterMass.lean 1 declarations
• SequenceSuccessfulWordImage.lean 1 declarations
• SequenceUniformInterval.lean 1 declarations
• SequentialHomLimit.lean 8 declarations
• SequentialModuleTail.lean 10 declarations
• SequentialRepresentationColimit.lean 8 declarations
• SequentialRepresentationDescent.lean 4 declarations
• SequentialRepresentationDiagram.lean 10 declarations
• SequentialRepresentationSteps.lean 7 declarations
• ShortSheetBridges.lean 2 declarations
• SignedPermutationCancellation.lean 1 declarations
• SimpleAlgebraAction.lean 3 declarations
• SimplyConnectedRetraction.lean 2 declarations
• SingleRowsTotal.lean 9 declarations
• SlowPositiveSelection.lean 2 declarations
• SmallCoefficientConstants.lean 16 declarations
• SmallCoefficientFiniteIndex.lean 6 declarations
• SmallCoefficientIdentityCycle.lean 7 declarations
• SmallCoefficientIdentityDimension.lean 2 declarations
• SmallCoefficientRationalRetract.lean 5 declarations
• SmallCoefficientTensorAlgebra.lean 11 declarations
• SmallDistanceRatio.lean 1 declarations
• SmallEigenlineCones.lean 2 declarations
• Solvable.lean 4 declarations
• SolvableFaithfulRepresentation.lean 5 declarations
• SolvableFiniteExtension.lean 3 declarations
• SolvableIntegerQuotient.lean 4 declarations
• SolvableLinearStructure.lean 2 declarations
• SolvablePolynomialGrowthPolycyclic.lean 3 declarations
• SolvableRepresentationAnnihilator.lean 2 declarations
• SolvableSubgroupFiniteExtension.lean 2 declarations
• SourceBundleStates.lean 7 declarations
• SpectralConjugation.lean 2 declarations
• SpectralLogValue.lean 7 declarations
• SpectralUnitGroup.lean 8 declarations
• SplitAnnihilator.lean 4 declarations
• SplitFactorTopology.lean 7 declarations
• SplitKernelCoordinates.lean 2 declarations
• SquareZeroPower.lean 2 declarations
• SubexponentialBounds.lean 10 declarations
• SubexponentialOperations.lean 5 declarations
• SubexponentialPolynomialValues.lean 1 declarations
• SubexponentialSections.lean 1 declarations
• SubgroupExtensionSection.lean 1 declarations
• SubgroupInductionCoordinates.lean 19 declarations
• SubgroupInductionExact.lean 8 declarations
• SubgroupShapiro.lean 3 declarations
• SubgroupShapiroReturn.lean 1 declarations
• SuccessfulBundleStates.lean 2 declarations
• SuccessfulParameterMass.lean 1 declarations
• SuccessfulSourceWord.lean 1 declarations
• SuccessfulWordImage.lean 1 declarations
• SurjectiveColumns.lean 1 declarations
• SuspendedVectorFieldBracket.lean 5 declarations
• SwitchBounds.lean 3 declarations
• SwitchParameterPullback.lean 3 declarations
• TemplateComparisonTranslation.lean 2 declarations
• TemplateConeTraceSeparation.lean 1 declarations
• TemplateConeTraces.lean 5 declarations
• TemplateInverseRays.lean 1 declarations
• TemplateSymmetries.lean 3 declarations
• TemplateThickeningLimit.lean 1 declarations
• TemplateVariationEquality.lean 1 declarations
• TensorFiniteDimension.lean 2 declarations
• TensorMultilinearGenerators.lean 3 declarations
• TerminalTupleProjection.lean 5 declarations
• ThreeCongruenceMatrix.lean 8 declarations
• ThreePrimitiveIntegerFamily.lean 1 declarations
• TopOrientationAutomorphisms.lean 1 declarations
• TorsionEigenvaluesUnipotentPower.lean 3 declarations
• TorsionFreeAbelianRank.lean 3 declarations
• TorsionFreeCyclicExtension.lean 3 declarations
• TorsionMatrixExponent.lean 2 declarations
• TorsionSpectrumFiniteTrace.lean 3 declarations
• TrajectoryProductLimits.lean 1 declarations
• TranscendentalExpandingEmbedding.lean 2 declarations
• TransferredAction.lean 8 declarations
• TransferredPairRepresentatives.lean 1 declarations
• TranslationLocalHomeomorph.lean 2 declarations
• TransverseEigenlineFreePair.lean 1 declarations
• TrivialBarCoinvariants.lean 4 declarations
• TrivialCentralLayerDerived.lean 1 declarations
• TruncatedEnvelopingAlgebra.lean 9 declarations
• TruncatedEnvelopingDerivation.lean 5 declarations
• TruncatedPrimitiveCoefficients.lean 4 declarations
• TruncatedRationalScalars.lean 5 declarations
• TupleBarDeterminant.lean 4 declarations
• TupleBarExteriorProduct.lean 6 declarations
• TupleBarInsertion.lean 4 declarations
• TupleBarPrepend.lean 5 declarations
• TupleBarProduct.lean 8 declarations
• TupleBarProductNaturality.lean 6 declarations
• TupleBarProductPrism.lean 4 declarations
• TupleCoordinateBounds.lean 2 declarations
• TupleLiftProjection.lean 2 declarations
• TuplePrism.lean 14 declarations
• TwistedBilateralDifference.lean 14 declarations
• TwistedBilateralRepresentation.lean 3 declarations
• TwistedBilateralSequence.lean 4 declarations
• TwoImageLimits.lean 5 declarations
• UltrafilterIndexBound.lean 1 declarations
• UltrafilterSubgroup.lean 3 declarations
• UnconditionalNilpotentCoordinates.lean 1 declarations
• UnconditionalNilpotentModel.lean 3 declarations
• UniformCoordinateGeneration.lean 1 declarations
• UniformCosetBound.lean 3 declarations
• UniformDynkinDifference.lean 1 declarations
• UniformDynkinProducts.lean 3 declarations
• UniformInteriorSlack.lean 1 declarations
• UniformLocalVirtualSolvability.lean 1 declarations
• UniformMonoidAlgebraGenerators.lean 1 declarations
• UniformOccupationAverage.lean 3 declarations
• UniformPolynomialGrowth.lean 6 declarations
• UniformSelection.lean 2 declarations
• UniformUnitNetBound.lean 1 declarations
• UnipotentCyclicEmbedding.lean 4 declarations
• UnipotentExtensionNilpotence.lean 1 declarations
• UnipotentFactorSystem.lean 2 declarations
• UnipotentGroupNilpotent.lean 11 declarations
• UnipotentProducts.lean 5 declarations
• UnitNetPartition.lean 15 declarations
• UnitParameterInverse.lean 1 declarations
• UnitaryCentralFixed.lean 8 declarations
• UnitaryCocycle.lean 5 declarations
• UnitaryEnergyProjection.lean 10 declarations
• UnitaryLazyEnergy.lean 11 declarations
• UnitaryMautner.lean 6 declarations
• UnitaryQuotientCocycle.lean 7 declarations
• UnitarySubspaceAction.lean 5 declarations
• UniversalCoefficientStability.lean 3 declarations
• UniversalDynkinTruncation.lean 2 declarations
• UniversalLogarithmWordCoefficients.lean 2 declarations
• UpperCentralLayerMap.lean 7 declarations
• ValuedConjugateFreePair.lean 5 declarations
• ValuedDiagonalDominance.lean 2 declarations
• ValuedEigenlineCones.lean 9 declarations
• ValuedEigenlineFreePair.lean 3 declarations
• ValuedIrreducibleFreePair.lean 3 declarations
• ValuedPowerDominant.lean 2 declarations
• VandermondeSubmoduleInterpolation.lean 5 declarations
• VectorSwitchParameters.lean 2 declarations
• VirtualNilpotentByAbelian.lean 2 declarations
• VirtualNilpotentNormalCore.lean 1 declarations
• VirtualNilpotentStableBase.lean 1 declarations
• VirtualSolvableDimension.lean 4 declarations
• VirtuallyMetabelianRecognition.lean 1 declarations
• VirtuallyUnipotentCommutatorAction.lean 2 declarations
• WeakDirectionalLinearity.lean 2 declarations
• WellFoundedModuleRelations.lean 5 declarations
• WordBasisCoordinates.lean 6 declarations
• WordCoefficientAgreement.lean 7 declarations
• WordCutCounting.lean 2 declarations
• WordExponentBounds.lean 3 declarations
• WordExponents.lean 6 declarations
• WordExtension.lean 6 declarations
• WordInteriorSlack.lean 1 declarations
• WordLengthFiltration.lean 7 declarations
• WordMinimumDegree.lean 4 declarations
• WordPivotCoordinates.lean 1 declarations
• WordPowerCoefficientBound.lean 1 declarations
• WordSplits.lean 6 declarations
• WordTensorConvolution.lean 6 declarations