prime_pow_dvd_iff_le — Mathlib

English

Let m be a nonzero Associate and p irreducible. Then p^k ≤ m iff k ≤ count p m.factors, with an explicit decidability assumption.

Русский

Для m ≠ 0 и неприводимого p, p^k ≤ m эквивалентно k ≤ count p m.factors (с учетом декидируемости).

LaTeX

$$$$m \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow p^k \\le m \\iff k \\le \\mathrm{count}(p,m.factors).$$$$

Lean4

theorem prime_pow_dvd_iff_le {m p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} :
    p ^ k ≤ m ↔ k ≤ count p m.factors := by rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount h₁]

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