All.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.All
0 declarations indexed from sourceView source ↗
Module documentation
Ramification of equal-characteristic Lubin–Tate extensions
Collects primitive points, their Galois displacements, and the resulting lower ramification groups.
Imports5
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.Core
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.DisplacementValuation
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.GaloisAction
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.LowerGroups
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.PrimitivePoint
This module has no indexed declarations. Its imports and full source are available here.