count_le_count_of_factors_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem count_le_count_of_factors_le {a b p : Associates α} (hb : b ≠ 0) (hp : Irreducible p)
    (h : a.factors ≤ b.factors) : p.count a.factors ≤ p.count b.factors :=
  by
  by_cases ha : a = 0
  · simp_all
  obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha
  obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb
  rw [h_sa, h_sb] at h ⊢
  rw [count_some hp, count_some hp]; rw [WithTop.coe_le_coe] at h
  exact Multiset.count_le_of_le _ h

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