prod_dvd_prod_of_subset — Mathlib

English

Let s ⊆ t be finite subsets of ι and f: ι → M with M a commutative monoid. Then (∏_{i ∈ s} f(i)) divides (∏_{i ∈ t} f(i)).

Русский

Пусть s ⊆ t — конечные подмножества ι и f: ι → M в коммутативном моноиде M. Тогда (∏_{i ∈ s} f(i)) делится на (∏_{i ∈ t} f(i)).

LaTeX

$$$$s \subseteq t \Rightarrow \left(\prod_{i \in s} f(i)\right) \mid \left(\prod_{i \in t} f(i)\right).$$$$

Lean4

theorem prod_dvd_prod_of_subset {ι M : Type*} [CommMonoid M] (s t : Finset ι) (f : ι → M) (h : s ⊆ t) :
    (∏ i ∈ s, f i) ∣ ∏ i ∈ t, f i :=
  Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| by simpa

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