All.lean
Nyll.ClassFieldTheory.KroneckerWeber.All
0 declarations indexed from sourceView source ↗
Module documentation
Kronecker–Weber and cyclotomic class fields
Collects the local cyclotomic embeddings, inertia bounds, and rational ray class comparisons used in the Kronecker–Weber theorem.
Imports15
- Nyll.ClassFieldTheory.KroneckerWeber.Core
- Nyll.ClassFieldTheory.KroneckerWeber.Final
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumCyclotomicTarget
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumGlobalEmbedding
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumLeftFactors
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumLocalizationEmbedding
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumValuationInertiaBound
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumValuedEmbedding
- Nyll.ClassFieldTheory.KroneckerWeber.GlobalPadicPrimePowInertiaBound
- Nyll.ClassFieldTheory.KroneckerWeber.LocalCyclotomicEmbedding
- Nyll.ClassFieldTheory.KroneckerWeber.RationalCyclotomicArithmeticReciprocity
- Nyll.ClassFieldTheory.KroneckerWeber.RationalRayClassFieldCyclotomic
- Nyll.ClassFieldTheory.KroneckerWeber.RayClassComparison
- Nyll.ClassFieldTheory.KroneckerWeber.Setup
- Nyll.ClassFieldTheory.KroneckerWeber.UnramifiedCompositumSupport
Imported by1
This module has no indexed declarations. Its imports and full source are available here.