dvd_iff_padicValNat_ne_zero — Mathlib

English

For prime p and n ≠ 0, p divides n iff padicValNat p n ≠ 0.

Русский

Для p простого и n ≠ 0, p делит n тогда и только тогда, когда padicValNat p n ≠ 0.

LaTeX

$$$p\mid n \iff \mathrm{padicValNat}(p,n) \neq 0$ (при $n\neq 0$, prime p)$$

Lean4

theorem dvd_iff_padicValNat_ne_zero {p n : ℕ} [Fact p.Prime] (hn0 : n ≠ 0) : p ∣ n ↔ padicValNat p n ≠ 0 :=
  ⟨fun h => one_le_iff_ne_zero.mp (one_le_padicValNat_of_dvd hn0 h), fun h =>
    Classical.not_not.1 (mt padicValNat.eq_zero_of_not_dvd h)⟩

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