All.lean
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.CyclotomicNorm.All
0 declarations indexed from sourceView source ↗
Module documentation
Norm groups of p-adic cyclotomic extensions
The prime-power and prime-to-p norm-subgroup computations used by local Kronecker--Weber, exposed as reusable finite local class field theory.
Imports3
This module has no indexed declarations. Its imports and full source are available here.