English
The v-adic completion of a number field is a normed field.
Русский
V-адик завершение числового поля является нормированным полем.
LaTeX
$$$\text{NormedField}((v.adicCompletion\ K))$$$
Lean4
noncomputable instance instRankOneValuedAdicCompletion :
Valuation.RankOne (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
where
hom :=
{ toFun := toNNReal (absNorm_ne_zero v)
map_zero' := rfl
map_one' := rfl
map_mul' := MonoidWithZeroHom.map_mul (toNNReal (absNorm_ne_zero v)) }
strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
exists_val_nontrivial :=
by
rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
use x
dsimp [adicCompletion]
rw [valuedAdicCompletion_eq_valuation' v (x : K)]
constructor
· simpa only [ne_eq, map_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff]
· apply ne_of_lt
rwa [valuation_of_algebraMap, intValuation_lt_one_iff_mem]
