pow_succ_padicValNat_not_dvd — Mathlib

English

Let p be a prime and n a nonzero natural number. Then p raised to the power (v_p(n) + 1) does not divide n, where v_p(n) is the p-adic valuation of n.

Русский

Пусть p — простое число, а n — ненулевое натуральное число. Тогда p^{v_p(n)+1} не делит n, где v_p(n) — p-адическая оценка числа n.

LaTeX

$$$\\forall p,n \\in \\mathbb{N},\\ p\\text{ prime} \\wedge n \\neq 0 \\Rightarrow p^{\\operatorname{padicValNat}(p,n)+1} \\nmid n$$$

Lean4

theorem pow_succ_padicValNat_not_dvd {n : ℕ} [hp : Fact p.Prime] (hn : n ≠ 0) : ¬p ^ (padicValNat p n + 1) ∣ n :=
  by
  rw [padicValNat_dvd_iff_le hn, not_le]
  exact Nat.lt_succ_self _

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