All.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.All
0 declarations indexed from sourceView source ↗
Module documentation
Global class fields
This public root exports the finite abelian class-field correspondence for closed finite-index idèle-class subgroups, exact conductor and ramification theory, and the actual big and small Hilbert class fields with their maximality and reciprocity characterizations.
Imports77
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianConductorExactness
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianConductorRamification
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianLocalConductorComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianNormConductor
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticClassFieldCorrespondence
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticHilbertClassFieldReciprocity
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticRayClassFieldReciprocity
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ArithmeticUnramifiedPrimeArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldMathlibArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldNaturality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldOverOriginalBase
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClassFieldRealization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldConstruction
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldNormRange
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldOriginalField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldReciprocity.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.Conductor
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorFrobenius
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorInfinitePart
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorLattice
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorLocalComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorPrimeArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorRayClassMaximality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorSupport
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicConductorUniqueness
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicNormConductor
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicNormTower
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclicRayClassMaximality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.CyclotomicKummerNormDescent
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.EmbeddedAbelianSubextension
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldContainment
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldCorrespondence
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldCorrespondenceTopology
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteIndexNormClassField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FinitePlaceArtinQuotient
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FullConductorRayClassField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldMaximalSubextension
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldMaximality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldPrimeSplitting
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldRealization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldReciprocity.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldUnramifiedMaximality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertNormCharacterization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.InfiniteAbelianClassFieldCorrespondence
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.KummerNormDescent
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.MathlibFrobeniusHilbertComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.MathlibGlobalReciprocity
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormConductor
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormLimitation
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormRayClassMaximality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormTowerConductor
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.OrdinaryNormClassField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PowerCongruenceCore
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealArtinKernelComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealNormArtinKernel
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealNormQuotientComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicRayClassComparison
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RationalRayPrimeClass
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassFieldRealization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassModulusProjection
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassPrimeIdele
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassSubgroupFieldAntitone
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassSubgroupPrimeArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayFrobeniusRigidity
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayPrimeGeneration
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SUnitKummerNormCore
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SUnitKummerNormRealization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldMaximalSubextension
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldNaturality
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldOverOriginalBase
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldMathlibArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertNormCharacterization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.UnramifiedPrimeArtin
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.UnramifiedPrimeNormClass
Imported by1
This module has no indexed declarations. Its imports and full source are available here.