Number theory · existing Mathlib declaration

Ostrowski's Theorem

Every nontrivial real-valued absolute value on the rational numbers measures size in one of two ways up to rescaling: like the usual real absolute value, or like the p-adic absolute value for one uniquely determined prime p.

Ostrowski's theorem
absolute values
equivalent absolute values
Archimedean absolute value
p-adic absolute value
rational numbers

The theorem at a glance

Ostrowski's theorem — the real class or one unique p-adic class

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory number-theory poster states that every nontrivial absolute value from the rationals to the reals is equivalent, not equal, to the standard real absolute value or to the p-adic absolute value for one unique prime. — Over ℚ with values in ℝ, every nontrivial absolute value belongs to the standard real equivalence class or to one uniquely determined p-adic class.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

One absolute-value gauge on Q branches into a blue real-line scale or a green nested p-adic ball tree with one prime p highlighted. — A nontrivial absolute value on Q is archimedean or p-adic up to equivalence.

Complementary intuition

A mathematical landmark

Ostrowski's theorem gives the definitive classification of nontrivial real-valued absolute values on ℚ, separating the familiar Archimedean size from the p-adic sizes that organize local number theory.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem Rat.AbsoluteValue.equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) : f ≈ real ∨ ∃! p, ∃ (_ : Fact p.Prime), f ≈ (padic p)

Selected evidence declaration text

theorem Rat.AbsoluteValue.equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) : f ≈ real ∨ ∃! p, ∃ (_ : Fact p.Prime), f ≈ (padic p)

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's classification of nontrivial absolute values f : AbsoluteValue ℚ ℝ. The conclusion is equivalence, not equality: f is equivalent to the standard real absolute value, or there is a unique natural number p carrying a prime instance for which f is equivalent to the p-adic absolute value. The declaration concerns ℚ with values in ℝ; it does not classify absolute values over arbitrary global fields or valuations with arbitrary codomains.

Equivalent absolute values need not be equal; equivalence preserves comparisons of sizes and, here, corresponds to positive-power rescaling.
The theorem assumes the absolute value is nontrivial.
The selected declaration is over ℚ with codomain ℝ, not over arbitrary global fields or arbitrary valuation codomains.
It is not a product formula, completion theorem, or algorithm for finding a prime from numerical samples.
ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.

Provenance

Origin and evidence stay separate

Existing declaration: Rat.AbsoluteValue.equiv_real_or_padic in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.ostrowski-theorem.v001
Source handling: Verified upstream reference; no mirrored source package