factorMultiset_le_iff' — Mathlib

English

A refinement of the previous equivalence, relating inequality to divisibility via a reformulation with v.prod.

Русский

Уточнение эквивалентности: неравенство сопоставляется делимости через произведение v.

LaTeX

$$$ {m : \\mathbb{N}_{+}} {v : \\text{PrimeMultiset}} : factorMultiset m \\le v \\iff m \\mid v.prod $$$

Lean4

theorem factorMultiset_le_iff' {m : ℕ+} {v : PrimeMultiset} : factorMultiset m ≤ v ↔ m ∣ v.prod :=
  by
  let h := @factorMultiset_le_iff m v.prod
  rw [v.factorMultiset_prod] at h
  exact h

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