equiv_real_or_padic — Mathlib

English

The real absolute value is not equivalent to any p-adic absolute value.

Русский

Действительное абсолютное значение не эквивалентно ни одному p-адическому значению.

LaTeX

$$¬ real.IsEquiv (padic p)$$

Lean4

/-- **Ostrowski's Theorem**: every absolute value (with values in `ℝ`) on `ℚ` is equivalent
to either the standard absolute value or a `p`-adic absolute value for a prime `p`. -/
theorem equiv_real_or_padic (f : AbsoluteValue ℚ ℝ) (hf_nontriv : f.IsNontrivial) :
    f ≈ real ∨ ∃! p, ∃ (_ : Fact p.Prime), f ≈ (padic p) :=
  by
  by_cases bdd : ∀ n : ℕ, f n ≤ 1
  · exact .inr <| equiv_padic_of_bounded hf_nontriv bdd
  · exact .inl <| equiv_real_of_unbounded bdd

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