All.lean
Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.All
0 declarations indexed from sourceView source ↗
Module documentation
Infinite local class field theory
Public aggregate for the topological profinite completion, compatible finite Artin maps, the absolute local Artin map, and the profinite local reciprocity equivalence.
Imports13
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteArtin
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteArtinRestriction
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteFiniteQuotientTransitions
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteFiniteQuotients
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbsoluteGaloisAbelianization
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.AbstractProfiniteCompletionComparison
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.FiniteAbelianQuotientKernels
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.FiniteReciprocityDiagram
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.LocalMultiplicativeCompletion
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletion
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletionCriteria
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteLocalReciprocity
- Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.TopologicalAbelianizationCongr
Imported by1
This module has no indexed declarations. Its imports and full source are available here.