padicValuation_cast — Mathlib

English

For any prime p and integer x, the p-adic valuation of x considered as a rational equals the p-adic valuation of x in the integers, i.e., v_p^{ℚ}(Int.cast x) = v_p^{ℤ}(x).

Русский

Для любого простого p и целого x p-адическая оценка x, рассматриваемого как рациональное число, совпадает с оценкой на целых: v_p^{ℚ}(x) = v_p^{ℤ}(x).

LaTeX

$$$\\operatorname{padicValuation}_{ℚ}(p, \\operatorname{Int.cast}(x)) = \\operatorname{padicValuation}_{ℤ}(p, x)$$$

Lean4

theorem padicValuation_cast (p : ℕ) [Fact p.Prime] (x : ℤ) :
    Rat.padicValuation p (Int.cast x) = Int.padicValuation p x :=
  rfl

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