All.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.All
0 declarations indexed from sourceView source ↗
Module documentation
Ideles and idele classes
Public aggregate for the idele group and the idele class group of a number field.
Imports26
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.BaseChange
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Basic
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.FiniteMathlibTopologyComparison
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.FinitePrime
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.IdealMap
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.IdentityComponent
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.LocallyCompact
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Norm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormApproximation.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormCore
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormOneCompact
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormTopology.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PositiveArchimedeanSection
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Principal
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PrincipalCore
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PrincipalNorm
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PrincipalTopology
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Relative.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.RestrictedProductUnitsTopology
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SPlaces
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SinglePlace
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SufficientlyLarge
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Topology
Imported by1
This module has no indexed declarations. Its imports and full source are available here.