English
If f and g are multiplicative and n is squarefree, then (f+g) on prime factors multiplies to (f*g)(n).
Русский
Если f и g мультипликативны и n квадратно без повторов, то произведение по простым делителям даёт сумму на функции, соответсвующее произведение f и g.
LaTeX
$$$\sum_{\text{prime powers}} (f+g) \text{ на квадратно-безповторном } n$ equals $(f*g)(n)$$$
Lean4
theorem prodPrimeFactors_add_of_squarefree [CommSemiring R] {f g : ArithmeticFunction R} (hf : IsMultiplicative f)
(hg : IsMultiplicative g) {n : ℕ} (hn : Squarefree n) : ∏ᵖ p ∣ n, (f + g) p = (f * g) n :=
by
rw [prodPrimeFactors_apply hn.ne_zero]
simp_rw [add_apply (f := f) (g := g)]
rw [Finset.prod_add, mul_apply, sum_divisorsAntidiagonal (f · * g ·), ← divisors_filter_squarefree_of_squarefree hn,
sum_divisors_filter_squarefree hn.ne_zero, factors_eq]
apply Finset.sum_congr rfl
intro t ht
rw [t.prod_val, Function.id_def, ← prod_primeFactors_sdiff_of_squarefree hn (Finset.mem_powerset.mp ht),
hf.map_prod_of_subset_primeFactors n t (Finset.mem_powerset.mp ht), ←
hg.map_prod_of_subset_primeFactors n (_ \ t) Finset.sdiff_subset]
