English
For a multiset s of natural numbers, the divisors of the product of all elements in s equal the product (in Finset sense) of the divisors of each element: divisors(s.prod) = (s.map divisors).prod.
Русский
Для мультиcета s натуральных чисел делители произведения всех элементов равны произведению делителей каждого элемента: divisors(s.prod) = (s.map divisors).prod.
LaTeX
$$$\\operatorname{divisors}(\\prod s)= (\\,s\\mapsto \\operatorname{divisors}\\,).prod$; more explicitly, $\\operatorname{divisors}(\\prod s)=\\left(\\operatorname{map}(\\operatorname{divisors}, s)\\right).\\operatorname{prod}$.$$
Lean4
theorem nat_divisors_prod (s : Multiset ℕ) : divisors s.prod = (s.map divisors).prod :=
map_multiset_prod Nat.divisorsHom s
