All.lean
Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Global class field theory
This module collects finite ideal-theoretic reciprocity and the topological maximal-abelian statements. The latter are proved via topological comparison with the existing restricted-product implementation.
Imports10
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FiniteAbelianGlobalReciprocity
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FiniteAbelianGlobalReciprocityQuotient
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FiniteAbelianReciprocityQuotientEquivMk
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceLocalGlobalNormKernel
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceRayArtinNormKernel
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceRayArtinDecomposition
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceCompletionLocalArtin
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceRayArtinLocalValue
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.TopologicalGlobalReciprocity
- Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.MaximalAbelianGlobalArtin
Imported by1
This module has no indexed declarations. Its imports and full source are available here.