image — Mathlib

English

The image of padicNormE on nonzero Padic elements is discrete in the sense it matches p-power valuations: there exists an integer n with ‖q‖ = (p^(-n)).

Русский

Образ padicNormE на ненулевых элементах Padic фиксирует дискретность норм через оценку p-степеней: существует целое n такое, что ‖q‖ = p^(−n).

LaTeX

$$$\exists n ∈ \mathbb{Z}, \|q\| = (p : \mathbb{Q})^{(-n)}$ for q ≠ 0$$

Lean4

protected theorem image {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, ‖q‖ = ↑((p : ℚ) ^ (-n)) :=
  Quotient.inductionOn q fun f hf ↦
    have : ¬f ≈ 0 := (PadicSeq.ne_zero_iff_nequiv_zero f).1 hf
    let ⟨n, hn⟩ := PadicSeq.norm_values_discrete f this
    ⟨n, by rw [← hn]; rfl⟩

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