All.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.All
0 declarations indexed from sourceView source ↗
Module documentation
Equal-characteristic Lubin--Tate formal modules
Public aggregate for the Lubin--Tate action and its division-module endomorphisms.
Imports4
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.AmbientBracketAction
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.DivisionModuleEndomorphisms
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.LubinTateAction
- Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.LubinTateEndomorphism
This module has no indexed declarations. Its imports and full source are available here.