nat_divisors_prod — Mathlib

English

Let s be a finite set and f a function on the index set; then divisors of the product ∏i∈s f(i) equal the product ∏i∈s divisors(f(i)).

Русский

Пусть s — конечное множество и f — функция. Тогда делители произведения \\prod_{i∈s} f(i) равны произведению делителей каждого f(i).

LaTeX

$$$\\operatorname{divisors}\\left(\\prod_{i\\in s} f(i)\\right) = \\prod_{i\\in s} \\operatorname{divisors}(f(i)).$$$

Lean4

theorem nat_divisors_prod {ι : Type*} (s : Finset ι) (f : ι → ℕ) : divisors (∏ i ∈ s, f i) = ∏ i ∈ s, divisors (f i) :=
  map_prod Nat.divisorsHom f s

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