count_eq_zero_of_ne — Mathlib

English

If p ≠ q are irreducible, then the count of q in p.factors is zero.

Русский

Если p и q различны и неприводимы, то count q в p.factors равен 0.

LaTeX

$$$$\\mathrm{Irreducible}(p) \\land \\mathrm{Irreducible}(q) \\land p \\neq q \\Rightarrow p.\\mathrm{count}(q.factors) = 0.$$$$

Lean4

theorem count_eq_zero_of_ne {p q : Associates α} (hp : Irreducible p) (hq : Irreducible q) (h : p ≠ q) :
    p.count q.factors = 0 :=
  not_ne_iff.mp fun h' ↦ h <| associated_iff_eq.mp <| hp.associated_of_dvd hq <| le_of_count_ne_zero hq.ne_zero hp h'

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