padicValInt_dvd_iff — Mathlib

English

For p prime, (p^n) divides a in integers iff a is zero or n ≤ v_p(a).

Русский

Пусть p простое. Тогда (p^n) делит a ∈ ℤ тогда и только тогда, когда a = 0 или n ≤ v_p(a).

LaTeX

$$$\\forall n,a \\in \\mathbb{N},\\ (p : \\mathbb{Z})^n \\mid a \\iff a=0 \\lor n \\le \\operatorname{padicValInt} p a$$$

Lean4

theorem padicValInt_dvd_iff (n : ℕ) (a : ℤ) : (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a := by
  rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff, ← Int.natCast_dvd, Int.natCast_pow]

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