is_rat — Mathlib

English

Let p be a prime and q a p-adic number. Then the p-adic norm of q is a rational number; i.e., there exists r ∈ ℚ with ‖q‖ = r.

Русский

Пусть p — простое число, q — p-адическое число. Тогда p-адическая норма ‖q‖ является рациональным числом; существует r ∈ ℚ such that ‖q‖ = r.

LaTeX

$$$\\forall p\\ (p\\text{ prime})\\ \\forall q \\in \\mathbb{Q}_p:\\ \\exists r \\in \\mathbb{Q},\\ \\|q\\| = r$$$

Lean4

protected theorem is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ‖q‖ = q' := by
  classical
    exact
    if h : q = 0 then ⟨0, by simp [h]⟩
    else
      let ⟨n, hn⟩ := padicNormE.image h
      ⟨_, hn⟩

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