All.lean
Nyll.ClassFieldTheory.LocalFieldTheory.All
0 declarations indexed from sourceView source ↗
Module documentation
Local field theory
Public root for reusable local-field infrastructure. This layer may depend on ValuationTheory, but not on RamificationTheory, ClassFormation, or LocalClassFieldTheory.
Imported by1
This module has no indexed declarations. Its imports and full source are available here.