padicValNat_dvd_iff_le — Mathlib

English

Let a ≠ 0. Then p^n ∣ a iff n ≤ padicValNat p a.

Русский

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

LaTeX

$$$ a \\neq 0 \\Rightarrow p^n \\mid a \\Leftrightarrow n \\le v_p(a) $$$

Lean4

theorem padicValNat_dvd_iff_le [hp : Fact p.Prime] {a n : ℕ} (ha : a ≠ 0) : p ^ n ∣ a ↔ n ≤ padicValNat p a := by
  rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity ha, Nat.cast_le]

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