dvd_iff_one_le_factorization — Mathlib

English

For prime p and n ≠ 0, p divides n if and only if 1 ≤ ν_p(n).

Русский

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

LaTeX

$$$$ p \text{ prime},\ n \neq 0 \Rightarrow p \mid n \iff 1 \le \nu_{p}(n). $$$$

Lean4

theorem dvd_iff_one_le_factorization {p n : ℕ} (pp : Prime p) (hn : n ≠ 0) : p ∣ n ↔ 1 ≤ n.factorization p :=
  Iff.trans (by simp) (pp.pow_dvd_iff_le_factorization hn)

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