padicValInt_mul_eq_succ — Mathlib

English

Let p be a prime and a an integer with a ≠ 0. Then the p-adic valuation satisfies v_p(a·p) = v_p(a) + 1.

Русский

Пусть p — простое число и a — целое число, не равное нулю. Тогда p-адическая оценка выполняется как v_p(a·p) = v_p(a) + 1.

LaTeX

$$$\\\\forall a \\,\\\\in \\\\mathbb{Z}, \\\\; a \\\\neq 0 \\\\Rightarrow \\\\mathrm{v}_p(a\\\\cdot p) = \\\\mathrm{v}_p(a) + 1$$$

Lean4

theorem padicValInt_mul_eq_succ (a : ℤ) (ha : a ≠ 0) : padicValInt p (a * p) = padicValInt p a + 1 :=
  by
  rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]
  simp only [padicValInt.of_nat, padicValNat_self]

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