values_discrete — Mathlib

English

For any nonzero q in ℚ, there exists an integer z such that padicNorm p q = (p:ℚ)^{-z}.

Русский

Для любого не нулевого q ∈ ℚ существует целое z, такое что padicNorm p q = (p:ℚ)^{-z}.

LaTeX

$$$ \exists z \in \mathbb{Z},\ padicNorm\ p\ q = (p: \mathbb{Q})^{-z} \quad \text{for } q \neq 0 $$$

Lean4

/-- `padicNorm p q` takes discrete values `p ^ -z` for `z : ℤ`. -/
protected theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padicNorm p q = (p : ℚ) ^ (-z) :=
  ⟨padicValRat p q, by simp [padicNorm, hq]⟩

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