theorem val_one_add_of_neg {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {a : F} (hva : v a < 0) : v (1 + a) = v a

If $v(a) < 0$, then $v(1+a) = v(a)$ by the ultrametric inequality applied to $\min(v(1), v(a)) = v(a)$.

theorem val_one_add_of_pos {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {a : F} (hva : 0 < v a) : v (1 + a) = 0

If $v(a) > 0$, then $v(1+a) = 0$ by the ultrametric inequality applied to $\min(v(1), v(a)) = 0$.

theorem one_add_ne_zero_of_neg_val' {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {a : F} (hva : v a < 0) : 1 + a ≠ 0

If $v(a) < 0$ then $1 + a \neq 0$: otherwise $v(1+a) = \infty$, contradicting $v(1+a) = v(a) < 0$.

theorem div_one_add_sub_one {F : Type u_1} [Field F] {a : F} (h : 1 + a ≠ 0) : a * (1 + a)⁻¹ - 1 = -(1 + a)⁻¹

Algebraic identity $\dfrac{a}{1+a} - 1 = -\dfrac{1}{1+a}$ valid whenever $1 + a \neq 0$.

theorem addval_finset_prod {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {ι : Type u_2} (f : ι → F) (s : Finset ι) : v (∏ i ∈ s, f i) = ∑ i ∈ s, v (f i)

An additive valuation turns finite products into finite sums: $v\!\left(\prod_{i \in s} f(i)\right) = \sum_{i \in s} v(f(i))$.

theorem addval_add_gt {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {x y : F} {N : ℤ} (hx : ↑N < v x) (hy : ↑N < v y) : ↑N < v (x + y)

Ultrametric inequality, threshold form: if $N < v(x)$ and $N < v(y)$ then $N < v(x+y)$.

theorem addval_sum_gt {F : Type u_1} [Field F] (v : AddValuation F (WithTop ℤ)) {ι : Type u_2} [DecidableEq ι] (f : ι → F) (s : Finset ι) {N : ℤ} (h : ∀ i ∈ s, ↑N < v (f i)) : ↑N < v (∑ i ∈ s, f i)

Threshold ultrametric inequality for finite sums: if $N < v(f(i))$ for all $i \in s$, then $N < v\!\left(\sum_{i \in s} f(i)\right)$.

theorem weak_approx_function_fields {F : Type u_1} [Field F] (n : ℕ) (v : Fin n → AddValuation F (WithTop ℤ)) (hv_surj : ∀ (i : Fin n), ∃ (u : F), (v i) u = ↑1) (hv_incomp : ∀ (i j : Fin n), i ≠ j → ¬∀ (x : F), 0 ≤ (v i) x → 0 ≤ (v j) x) (f : Fin n → F) (N : ℤ) : ∃ (g : F), ∀ (i : Fin n), ↑N < (v i) (g - f i)

Weak Approximation for Function Fields (Corollary 20.5). Given finitely many pairwise incomparable surjective discrete additive valuations $v_1, \ldots, v_n$ on a field $F$, target elements $f_1, \ldots, f_n \in F$ and any threshold $N \in \mathbb{Z}$, there exists a single $g \in F$ with $v_i(g - f_i) > N$ for every $i$.