ClassFieldTheory.rayLocalHigherUnitGroup_zero
At depth zero the local higher-unit group is the full group of integral units, not the full multiplicative group of the local field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u
open NumberField IsDedekindDomainLean source · statement
theorem rayLocalHigherUnitGroup_zero
{K : Type u} [Field K] [NumberField K]
(v : HeightOneSpectrum (𝓞 K)) :
rayLocalHigherUnitGroup v 0 =
(v.adicCompletionIntegers K).units