factorization_prime_le_iff_dvd — Mathlib

English

For nonzero d and n, d divides n if and only if for every prime p, the exponent of p in d is at most the exponent of p in n.

Русский

Для непустых d и n: d | n тогда и только тогда, когда для каждого простого p показатель степени p в d не превосходит показатель степени p в n.

LaTeX

$$$$\big(\forall p\text{ prime},\ \nu_p(d) \le \nu_p(n)\big) \iff d \mid n.$$$$

Lean4

theorem factorization_prime_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    (∀ p : ℕ, p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n :=
  by
  rw [← factorization_le_iff_dvd hd hn]
  refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩
  simp_rw [factorization_eq_zero_of_non_prime _ hp]
  rfl

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