All.lean
Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.All
0 declarations indexed from sourceView source ↗
Module documentation
Multiplicative evaluation of p-adic Lubin–Tate series
Collects finite-level evaluations and primitive roots together with completed coefficient evaluations, scalar endomorphisms, and primitive points.
Imports6
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedCoefficientEvaluation
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedPrimitivePoint
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedScalarEndomorphism
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.Core
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.FiniteLevelEvaluation
- Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.FiniteLevelPrimitiveRoot
Imported by1
This module has no indexed declarations. Its imports and full source are available here.