All.lean
Nyll.ClassFieldTheory.LocalFieldTheory.Padic.Cyclotomic.Unramified.All
0 declarations indexed from sourceView source ↗
Module documentation
Unramified p-adic cyclotomic extensions
The prime-to-p cyclotomic construction and its arithmetic Frobenius.
This module has no indexed declarations. Its imports and full source are available here.