Existing in Mathlib · Number theory
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
Exact theorem
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)The theorem at a glance
Ostrowski's theorem — the real class or one unique p-adic class
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Ostrowski's theorem — the real class or one unique p-adic class
Detailed visual description
The sparse engraved poster distinguishes equivalence from equality before splitting a rational fraction-wheel into the standard real class, whose values on natural numbers are unbounded, and one unique p-adic class, whose values on natural numbers are bounded above by one. Both branch labels explicitly name natural numbers; they do not assert that a p-adic absolute value is bounded on all of ℚ. The nested p-adic branch is centered on one gold prime, and the footer keeps the statement within ℚ and ℝ.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Ostrowski's Theorem — scientific diagram
Detailed visual description
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.
Why it matters
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.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
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.
Source and local evidence
Where the theorem comes from
- Existing declaration
Rat.AbsoluteValue.equiv_real_or_padicin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.ostrowski-theorem.v001