toFinset_prod_dvd_prod — Mathlib

English

Let S be a multiset in a commutative monoid. Then the product of the distinct elements of S (i.e., over S.toFinset) divides the product of all elements of S.

Русский

Пусть S — мультсет в коммутативном моноиде. Тогда произведение всех различных элементов S (то есть по S.toFinset) делит произведение всех элементов S (с учетом кратностей).

LaTeX

$$$\left(\prod x \in S.toFinset, x\right) \mid \left(\prod x \in S, x\right)$$$

Lean4

theorem toFinset_prod_dvd_prod [DecidableEq M] [CommMonoid M] (S : Multiset M) : S.toFinset.prod id ∣ S.prod :=
  by
  rw [Finset.prod_eq_multiset_prod]
  refine Multiset.prod_dvd_prod_of_le ?_
  simp [Multiset.dedup_le S]

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