All.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.All
0 declarations indexed from sourceView source ↗
Module documentation
Equal-characteristic Lubin--Tate theory
Public aggregate for the equal-characteristic Lubin--Tate construction. It includes the Laurent-series model, finite and completed Lubin--Tate levels, and the Frobenius and theta constructions. The local-class-field-theory norm-subgroup calculation and its transport live in LocalClassFieldTheory.LubinTateApplication.
Each mathematical stage has a reader-facing aggregate below LubinTate.EqualCharacteristic; declarations remain in the matching namespace.
Imports9
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Existence.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.All
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.RealIndexSteps
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Theta.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.