padicValuation_lt_one_iff — Mathlib

English

For any prime p and integer x, v_p^{ℤ}(x) < 1 if and only if p divides x.

Русский

Для любого p и целого x, v_p^{ℤ}(x) < 1 тогда и только тогда, когда p делит x.

LaTeX

$$v_p^{ℤ}(x) < 1 \\Leftrightarrow p \\mid x$$

Lean4

theorem padicValuation_lt_one_iff {p : ℕ} [Fact p.Prime] {x : ℤ} : Int.padicValuation p x < 1 ↔ (p : ℤ) ∣ x := by
  simp [lt_iff_le_and_ne, padicValuation_eq_one_iff, Int.padicValuation_le_one]

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