isNonarchimedean_adicAbvDef — Mathlib

English

The v-adic absolute value is non-archimedean: |x+y|_v ≤ max(|x|_v, |y|_v) for all x,y ∈ K, when 1 < b.

Русский

Адическая абсолютная величина по v является неархимова: |x+y|_v ≤ max(|x|_v, |y|_v) при любых x,y ∈ K при 1 < b.

LaTeX

$$IsNonarchimedean (α := K) (fun x => v.adicAbvDef hb x)$$

Lean4

theorem isNonarchimedean_adicAbvDef {b : NNReal} (hb : 1 < b) : IsNonarchimedean (α := K) (fun x ↦ v.adicAbvDef hb x) :=
  by
  intro x y
  simp only [adicAbvDef]
  have h_mono := (toNNReal_strictMono hb).monotone
  rw [← h_mono.map_max]
  exact h_mono ((v.valuation _).map_add x y)

Похожие утверждения