English
For a bounded and nontrivial absolute value f on Q, there exists a prime p such that f is equivalent to the p-adic one; otherwise f is equivalent to the real one.
Русский
Если ненулевое и ограниченное по модулю абсолютное значение f на Q эквивариантно p-адическому, тогда существует простое p. Иначе f эквівариантно к реальномуplace.
LaTeX
$$∃ p prime, f ≈ (padic p) ∨ f ≈ real$$
Lean4
/-- The equivalence class of an absolute value on the rationals is determined by its values on
the natural numbers. -/
theorem exists_nat_rpow_iff_isEquiv : (∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, f n ^ c = g n) ↔ f.IsEquiv g :=
by
rw [isEquiv_iff_exists_rpow_eq]
refine ⟨fun ⟨c, hc, h⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, h⟩ ↦ ⟨c, hc, (congrFun h ·)⟩⟩
ext1 x
rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den, ← apply_natAbs_eq, ←
apply_natAbs_eq, h (natAbs x.num)]
