All.lean
Nyll.ClassFieldTheory.LubinTate.Padic.All
0 declarations indexed from sourceView source ↗
Module documentation
P-adic Lubin--Tate theory
Aggregate for the multiplicative Lubin--Tate series and its completed-level, Frobenius, residue, fixed-field, and changed-uniformizer constructions.
Imports23
- Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerCoefficient
- Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerIntertwiner.All
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardCompositum
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardFixedField
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardFrobenius
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardResidue
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedStandardUnramified
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedUniformizerFixedField
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedUniformizerPrimitive
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedUniformizerThetaFixed
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedFrobeniusEvaluation
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedFrobeniusLift
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedLevel
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedPrimitiveAction
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedPrimitiveIrreducible
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedPrimitiveUniformizer
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedResidueFrobenius
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedStandardLevelTransport
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedUnramifiedField
- Nyll.ClassFieldTheory.LubinTate.Padic.CompletedUnramifiedFrobeniusFixed
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.All
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeIntertwiner
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeSeries
Imported by1
This module has no indexed declarations. Its imports and full source are available here.