padicValuation — Mathlib

English

For a prime p, the p-adic valuation on integers is obtained by transporting the p-adic valuation from rationals along the natural embedding ℤ → ℚ; i.e., v_p^{ℤ}(x) = v_p^{ℚ}(Int.cast x).

Русский

Для простого p p-адическая оценка на целых получается из рационального аналога через естественное вложение ℤ в ℚ: v_p^{ℤ}(x) = v_p^{ℚ}(x как целое)

LaTeX

$$v_p^{ℤ} = (v_p^{ℚ}) \\circ (\\iota: \\mathbb{Z} \\hookrightarrow \\mathbb{Q})$$

Lean4

/-- The p-adic valuation on integers, sending `p` to `(exp (-1) : ℤᵐ⁰)` -/
def padicValuation (p : ℕ) [Fact p.Prime] : Valuation ℤ ℤᵐ⁰ :=
  (Rat.padicValuation p).comap (Int.castRingHom ℚ)

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