All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.All
0 declarations indexed from sourceView source ↗
Module documentation
Ideles in finite extensions of number fields
Public aggregate for base change, extension, and norm maps on ideles and idele classes.
Imports15
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.BaseChange
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.ClassGroup
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.EmbeddingNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.GaloisDescent
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.GaloisNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdealClass
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleClassBaseChange
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleNormComponents
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.InfiniteOnePlaceBaseNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.LocalComponent
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.LocalNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormLocalOrder
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.NormProperties
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.OnePlaceBaseNorm
This module has no indexed declarations. Its imports and full source are available here.