All.lean
Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Local class-field definitions
This aggregate collects field norm maps, subgroups and quotients, finite abelian local extensions, open subgroups of finite index, and topological profinite completions.
Imports7
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormHom
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormQuotient
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FieldNormSubgroup
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.FiniteAbelianLocalExtension
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.IsFieldNorm
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.OpenFiniteIndexSubgroup
- Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.TopologicalProfiniteCompletion
Imported by1
This module has no indexed declarations. Its imports and full source are available here.