le_of_count_ne_zero — Mathlib

English

If count p m.factors ≠ 0 for an irreducible p and nonzero m, then p ≤ m in the natural divisibility order.

Русский

Если count p m.factors ≠ 0 тогда p ≤ m в порядке делимости, когда m ≠ 0 и p неприводим.

LaTeX

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

Lean4

theorem le_of_count_ne_zero {m p : Associates α} (h0 : m ≠ 0) (hp : Irreducible p) : count p m.factors ≠ 0 → p ≤ m :=
  by
  nontriviality α
  rw [← pos_iff_ne_zero]
  intro h
  rw [← pow_one p]
  apply (prime_pow_dvd_iff_le h0 hp).2
  simpa only

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