factorization_pos_of_dvd — Mathlib

English

If p is prime and p divides n with n ≠ 0, then 0 < n.factorization p.

Русский

Пусть p — простое и p делит n, при n ≠ 0, тогда 0 < n.factorization p.

LaTeX

$$$ 0 < n.factorization p $ (assuming $p$ prime and $n \neq 0$ and $p \mid n$)$$

Lean4

theorem factorization_pos_of_dvd {n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) : 0 < n.factorization p := by
  rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]

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