nat_divisors_prod — Mathlib

English

Let l be a finite list of natural numbers. Then the divisors of the product of the list equal the product (in Finset sense) of the divisors of each element: divisors(∏i li) = ∏i divisors(li).

Русский

Пусть l — конечный список чисел. Тогда делители произведения элементов списка равны произведению множеств делителей каждого элемента: divisors(∏ li) = ∏ li divisors(li).

LaTeX

$$$\\operatorname{divisors}\\left(\\prod_{i} l_i\\right)=\\prod_i\\operatorname{divisors}(l_i).$$$

Lean4

theorem nat_divisors_prod (l : List ℕ) : divisors l.prod = (l.map divisors).prod :=
  map_list_prod Nat.divisorsHom l

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