All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Algebraic number theory
Public root for the reusable global algebraic-number-theory layer used by class field theory. It exports finite abelian composita, idèles and idèle classes in extensions, normal-closure and splitting results, ray class groups, S-units, and the ramification and degree results needed by global applications.
Imports18
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.AdeleBaseChange
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.CompositumEmbedding
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.FiniteAbelianCompositum
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.FinitePlaceAdicCompletionCongrEquiv
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquivTopology
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NormalClosure
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.PowerResidueSymbols.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.QuadraticReciprocity
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.SeparableClosureEmbedding
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.TensorProduct
Imported by1
This module has no indexed declarations. Its imports and full source are available here.