LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

An absolute value is nonarchimedean exactly when every integer has absolute value at most one

Statement

Let $F$ be a field with absolute value $∣ \cdot ∣$ in the sense of Absolute values on a field. Then $∣ \cdot ∣$ is nonarchimedean if and only if

$∣ n \cdot 1_{F} ∣ \leq 1$

for every integer $n$ .

Facts & Assumptions

Given: A field $F$ and an absolute value $∣ \cdot ∣$ on $F$ .

[L1]

An absolute value is multiplicative and satisfies both the ordinary and, in the nonarchimedean case, the strong triangle inequality (Absolute values on a field).

Proof

technique · direct

1.1

Since $1_{F} \neq 0$ , multiplicativity in [L1] gives $∣ 1_{F} ∣ = ∣ 1_{F} ∣^{2}$ , hence $∣ 1_{F} ∣ = 1$ . Also $∣ - 1 ∣^{2} = ∣ 1 ∣ = 1$ , so $∣ - 1 ∣ = 1$ .

L1givenalgebra

1.2

Assume conversely that $∣ n 1_{F} ∣ \leq 1$ for every integer $n$ . Fix $x, y \in F$ and put $M : = \max {∣ x ∣, ∣ y ∣}$ . If $M = 0$ there is nothing to prove, so scale by a nonzero element and reduce to $M = 1$ . Then every binomial coefficient has absolute value at most $1$ , so $∣ (x + y)^{m} ∣ \leq \max_{0 \leq k \leq m} ∣ (\binom{m}{k}) ∣ ∣ x ∣^{k} ∣ y ∣^{m - k} \leq 1$ for every $m \geq 1$ . Hence $∣ x + y ∣^{m} \leq 1$ for all $m$ , so $∣ x + y ∣ \leq 1 = M$ . Undoing the scaling gives $∣ x + y ∣ \leq \max {∣ x ∣, ∣ y ∣}$ .

L1givenalgebra

2.1

Assume first that $∣ \cdot ∣$ is nonarchimedean. For $n \geq 1$ , induction using step 1.1 and $∣ (n + 1) 1_{F} ∣ \leq \max {∣ n 1_{F} ∣, ∣ 1_{F} ∣}$ gives $∣ n 1_{F} ∣ \leq 1$ . For negative $n$ , $∣ n 1_{F} ∣ = ∣ - 1 ∣ ∣ (- n) 1_{F} ∣ \leq 1$ , and $∣ 0 ∣ = 0 \leq 1$ .

L1step 1.1induction

3.1

Thus the integer bound implies the strong triangle inequality, and step 2.1 proved the reverse implication.

step 2.1step 1.2∎

Depends on

Absolute values on a field

Used by

Ostrowski's theorem for the rationals Theorem

Dependency tree · one level

1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Andrew V. Sutherland, 18.782 Lecture 5 (standard reference, not scraped)
J. S. Milne, Algebraic Number Theory, Chapter 7 (standard reference, not scraped)