All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.All
0 declarations indexed from sourceView source ↗
Module documentation
Adelic coordinates and restricted products
Imports9
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.Coordinates
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.FinitePlaceTensorBlock
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.FiniteRestrictedProductBaseChange
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.InfinitePlaceTensorBlock
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralLocalFactor
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.LocalComponents
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.RestrictedAction
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.RestrictedProduct
Imported by1
This module has no indexed declarations. Its imports and full source are available here.