All.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.All
0 declarations indexed from sourceView source ↗
Module documentation
Frobenius in equal-characteristic Lubin--Tate theory
Public aggregate for coefficient Frobenius, Laurent-series Frobenius, and the completed unramified field.
Imports4
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CoefficientFrobenius
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CompletedUnramifiedField
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.ContractingEquation
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.LaurentSeriesFrobenius
This module has no indexed declarations. Its imports and full source are available here.