All.lean
Nyll.SawinTotallyRealTowers.All
0 declarations indexed from sourceView source ↗
Module documentation
Totally real towers
Totally real number-field towers and their unramified pro-p Galois groups. Includes Frobenius constraints, finite-support comparisons and relation-rank bounds.
Imports84
- Nyll.SawinTotallyRealTowers.FinitePlaceDecompositionSplit
- Nyll.SawinTotallyRealTowers.FinitePlaceFrobenius
- Nyll.SawinTotallyRealTowers.FrobeniusWeightBudget
- Nyll.SawinTotallyRealTowers.RealProPDepthStage
- Nyll.SawinTotallyRealTowers.RealProPFrobenius
- Nyll.SawinTotallyRealTowers.RealProPFrobeniusCut
- Nyll.SawinTotallyRealTowers.RealProPFrobeniusStage
- Nyll.SawinTotallyRealTowers.RealProTwoDeepFrobenius
- Nyll.SawinTotallyRealTowers.RealProTwoFrobeniusSequence
- Nyll.SawinTotallyRealTowers.RealProTwoInitialPresentation
- Nyll.SawinTotallyRealTowers.SixPrimeFiniteSupport
- Nyll.SawinTotallyRealTowers.RealProTwoInitialGroup
- Nyll.SawinTotallyRealTowers.RealProTwoH2Bound
- Nyll.SawinTotallyRealTowers.RealProTwoH2AbsoluteKernel
- Nyll.SawinTotallyRealTowers.RealProPStageRestriction
- Nyll.SawinTotallyRealTowers.RealProPStageLocalConditions
- Nyll.SawinTotallyRealTowers.RealCharacterInertiaExistence
- Nyll.SawinTotallyRealTowers.RealCentralLiftCorrection
- Nyll.SawinTotallyRealTowers.RationalIdealSquareRadical
- Nyll.SawinTotallyRealTowers.NegativeThreeLocalRadical
- Nyll.SawinTotallyRealTowers.AbsoluteRealProPUnramified
- Nyll.SawinTotallyRealTowers.RealCharacterInertiaCorrection
- Nyll.SawinTotallyRealTowers.InfiniteArtinCompatibility
- Nyll.SawinTotallyRealTowers.FiniteKummerContinuousKernel
- Nyll.SawinTotallyRealTowers.AbsoluteCharacterRealValue
- Nyll.SawinTotallyRealTowers.FiniteKummerAbsoluteKernel
- Nyll.SawinTotallyRealTowers.FiniteRealPExtension
- Nyll.SawinTotallyRealTowers.FiniteRealPExtensionSupport
- Nyll.SawinTotallyRealTowers.GaloisPCompositum
- Nyll.SawinTotallyRealTowers.MaximalRealProPGroup
- Nyll.SawinTotallyRealTowers.MaximalRealProPOutside
- Nyll.SawinTotallyRealTowers.NegativeThreeCharacter
- Nyll.SawinTotallyRealTowers.QuadraticBasis
- Nyll.SawinTotallyRealTowers.QuadraticBasisDiscriminant
- Nyll.SawinTotallyRealTowers.QuadraticFieldDiscriminant
- Nyll.SawinTotallyRealTowers.QuadraticGenerator
- Nyll.SawinTotallyRealTowers.QuadraticIntegerBasis
- Nyll.SawinTotallyRealTowers.QuadraticIntegerRepresentation
- Nyll.SawinTotallyRealTowers.QuadraticIntegralCoordinates
- Nyll.SawinTotallyRealTowers.QuadraticIntegralGenerator
- Nyll.SawinTotallyRealTowers.QuadraticIntegralParity
- Nyll.SawinTotallyRealTowers.QuadraticReality
- Nyll.SawinTotallyRealTowers.QuadraticSquareClass
- Nyll.SawinTotallyRealTowers.QuadraticSquarefreeGenerator
- Nyll.SawinTotallyRealTowers.QuadraticSupportedGenerator
- Nyll.SawinTotallyRealTowers.QuadraticTrace
- Nyll.SawinTotallyRealTowers.RamificationSupport
- Nyll.SawinTotallyRealTowers.RamificationSupportCompositum
- Nyll.SawinTotallyRealTowers.RamificationSupportTransport
- Nyll.SawinTotallyRealTowers.RationalRamificationSupport
- Nyll.SawinTotallyRealTowers.RationalSquarefree
- Nyll.SawinTotallyRealTowers.RealCompositum
- Nyll.SawinTotallyRealTowers.RealProPOpenNormalStage
- Nyll.SawinTotallyRealTowers.SquarefreeIntegralCoordinates
- Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.All
- Nyll.SawinTotallyRealTowers.FiveQuadraticSquareClasses
- Nyll.SawinTotallyRealTowers.QuadraticAdmissibleLayer
- Nyll.SawinTotallyRealTowers.QuadraticClosure
- Nyll.SawinTotallyRealTowers.QuadraticClosureClassification
- Nyll.SawinTotallyRealTowers.QuadraticCompositum
- Nyll.SawinTotallyRealTowers.QuadraticSquareDescent
- Nyll.SawinTotallyRealTowers.SixPrimeQuadraticClassification
- Nyll.SawinTotallyRealTowers.SixPrimeQuadraticCompositum
- Nyll.SawinTotallyRealTowers.SixPrimeSquareClasses
- Nyll.SawinTotallyRealTowers.SixPrimeSupport
- Nyll.SawinTotallyRealTowers.FiveQuadraticDegree
- Nyll.SawinTotallyRealTowers.MultiquadraticAdjoin
- Nyll.SawinTotallyRealTowers.SixPrimeQuadraticExponent
- Nyll.SawinTotallyRealTowers.SquareRootAdjoin
- Nyll.SawinTotallyRealTowers.FixedFieldIntersection
- Nyll.SawinTotallyRealTowers.ProTwoFrattini
- Nyll.SawinTotallyRealTowers.RealProTwoFrattiniField
- Nyll.SawinTotallyRealTowers.RealProTwoQuadraticFixedFields
- Nyll.SawinTotallyRealTowers.RealProTwoFrattiniQuotient
- Nyll.SawinTotallyRealTowers.RealProTwoGeneratorRank
- Nyll.SawinTotallyRealTowers.AbsoluteRealKernelField
- Nyll.SawinTotallyRealTowers.AbsoluteRealProPRestriction
- Nyll.SawinTotallyRealTowers.AbsoluteRealProPFactor
- Nyll.SawinTotallyRealTowers.RealProTwoFreeSource
- Nyll.SawinTotallyRealTowers.RealProPFrobeniusFixedField
- Nyll.SawinTotallyRealTowers.RealProPFrobeniusFixedFieldSplitting
- Nyll.SawinTotallyRealTowers.SawinDiscriminantBound
- Nyll.SawinTotallyRealTowers.SawinTotallyRealTower
- Nyll.SawinTotallyRealTowers.MartinetCorollary
Imported by1
This module has no indexed declarations. Its imports and full source are available here.