At a chosen finite place which is unramified in L, every concrete adic integer unit is an actual norm from the chosen localization.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
{K L : Type}
[Field K] [NumberField K]
[Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]Lean source · statement
theorem adicCompletionIntegerUnits_le_chosenFinitePlaceLocalNormSubgroup
(v₀ : HeightOneSpectrum (𝓞 K))
(hunram :
ChosenFinitePlaceIsUnramified
(K := K) (L := L) v₀) :
(v₀.adicCompletionIntegers K).units ≤
chosenFinitePlaceLocalNormSubgroup
(K := K) (L := L) v₀