All.lean
Nyll.ClassFieldTheory.LubinTate.FormalModule.All
0 declarations indexed from sourceView source ↗
Module documentation
Lubin--Tate formal modules
Public aggregate for the formal-series constructions used by Lubin--Tate theory: composition, linear terms, intertwiners, coefficient equations, reduction, the standard Lubin--Tate series, and the coefficientwise recursive existence-and-uniqueness construction, including the resulting standard commutative formal group and its coefficient-ring endomorphisms.
Imports11
- Nyll.ClassFieldTheory.LubinTate.FormalModule.CoefficientEquation
- Nyll.ClassFieldTheory.LubinTate.FormalModule.DegreeStabilization
- Nyll.ClassFieldTheory.LubinTate.FormalModule.Intertwiner
- Nyll.ClassFieldTheory.LubinTate.FormalModule.LinearTerm
- Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveCoefficient
- Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveCorrection
- Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveIntertwiner
- Nyll.ClassFieldTheory.LubinTate.FormalModule.Reduction
- Nyll.ClassFieldTheory.LubinTate.FormalModule.Series
- Nyll.ClassFieldTheory.LubinTate.FormalModule.StandardFormalGroup
- Nyll.ClassFieldTheory.LubinTate.FormalModule.StandardSeries
Imported by1
This module has no indexed declarations. Its imports and full source are available here.