All.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Global class field theory
This aggregate imports the implementation modules for global Artin reciprocity, the class-field correspondence, Hilbert and power-residue reciprocity, ideal Artin maps, decomposition, and principalization. Reader-facing statements are collected in ClassFieldTheory.Theorems.GlobalClassFieldTheory.All.
Imports5
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Cohomology.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.