All.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Existence.All
0 declarations indexed from sourceView source ↗
Module documentation
Equal-characteristic Laurent model for Lubin--Tate theory
Public aggregate for the reusable Laurent-series model and its normalized uniformizer. Transport of the exact norm-subgroup calculation to an arbitrary equal-characteristic local field uses finite local reciprocity and is exported by LocalClassFieldTheory.LubinTateApplication.
Imports3
This module has no indexed declarations. Its imports and full source are available here.