All.lean
Nyll.ClassFieldTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Class field theory
Local and global class field theory, including reciprocity laws, the class field axiom, Hasse–Arf and Kronecker–Weber. Supporting constructions cover idèles, Kummer theory and Lubin–Tate theory.
Imports13
- Nyll.ClassFieldTheory.Algebra.All
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.All
- Nyll.ClassFieldTheory.AlgebraicNumberTheory.All
- Nyll.ClassFieldTheory.Definitions.All
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.All
- Nyll.ClassFieldTheory.HasseArf
- Nyll.ClassFieldTheory.KroneckerWeber.All
- Nyll.ClassFieldTheory.KummerTheory.All
- Nyll.ClassFieldTheory.LocalClassFieldTheory.All
- Nyll.ClassFieldTheory.LocalFieldTheory.All
- Nyll.ClassFieldTheory.LubinTate.All
- Nyll.ClassFieldTheory.RamificationTheory.All
- Nyll.ClassFieldTheory.Theorems.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.