pow_dvd_iff_le_factorization — Mathlib

English

Let p be a prime. For n ≠ 0, p^k divides n if and only if k ≤ ν_p(n).

Русский

Пусть p — простое. Для n ≠ 0: p^k делит n тогда и только тогда, когда k ≤ ν_p(n).

LaTeX

$$$$ \forall p,k,n \in \mathbb{N},\ p \text{ prime} \Rightarrow n \neq 0 \Rightarrow p^{k} \mid n \iff k \le \nu_{p}(n). $$$$

Lean4

theorem pow_dvd_iff_le_factorization {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p := by
  rw [← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn, pp.factorization_pow, single_le_iff]

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