prod_dvd_prod_of_dvd — Mathlib

English

If f(i) divides g(i) for all i in s, then the product ∏_{i∈s} f(i) divides ∏_{i∈s} g(i).

Русский

Если для всех i ∈ s выполняется f(i) | g(i), то произведение ∏_{i∈s} f(i) делит произведение ∏_{i∈s} g(i).

LaTeX

$$$\\Bigl(\\forall i \\in s,\\ f(i) \\\\mid g(i)\\Bigr) \\Rightarrow \\prod_{i \\in s} f(i) \\\\mid \\prod_{i \\in s} g(i)$$$

Lean4

theorem prod_dvd_prod_of_dvd (f g : ι → M) (h : ∀ i ∈ s, f i ∣ g i) : ∏ i ∈ s, f i ∣ ∏ i ∈ s, g i :=
  Multiset.prod_dvd_prod_of_dvd _ _ h

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