padicValNat_dvd_iff — Mathlib

English

For any a,n, p^n ∣ a iff a = 0 or n ≤ v_p(a).

Русский

Для любых a,n: p^n делит a тогда либо a=0, либо n ≤ v_p(a).

LaTeX

$$$ p^n \\mid a \\Leftrightarrow a = 0 \\lor n \\le v_p(a) $$$

Lean4

theorem padicValNat_dvd_iff (n : ℕ) [hp : Fact p.Prime] (a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · exact iff_of_true (dvd_zero _) (Or.inl rfl)
  · rw [padicValNat_dvd_iff_le ha, or_iff_right ha]

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