count_le_count_of_le — Mathlib

English

If b ≠ 0, p is irreducible, and a ≤ b, then p.count a.factors ≤ p.count b.factors.

Русский

Если b ≠ 0, p неприводим и a ≤ b, то p.count a.factors ≤ p.count b.factors.

LaTeX

$$hb : b ≠ 0 → hp : Irreducible p → h : a ≤ b → p.count a.factors ≤ p.count b.factors$$

Lean4

theorem count_le_count_of_le {a b p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : a ≤ b) :
    p.count a.factors ≤ p.count b.factors :=
  count_le_count_of_factors_le hb hp <| factors_mono h

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