English
Let f be multiplicative. For a finite set s and a function g, if the g(i) are pairwise coprime, then f(∏_{i∈s} g(i)) = ∏_{i∈s} f(g(i)).
Русский
Пусть f — мультипликативна. Для конечного множества s и функции g, если числа g(i) попарно взаимно простые, то f(∏_{i∈s} g(i)) = ∏_{i∈s} f(g(i)).
LaTeX
$$$\displaystyle f\left(\prod_{i\in s} g(i)\right) = \prod_{i\in s} f(g(i))$ при парах взаимной простоты $(\forall i,j\in s, i\neq j \Rightarrow \gcd(g(i),g(j))=1)$$$
Lean4
theorem map_prod {ι : Type*} [CommMonoidWithZero R] (g : ι → ℕ) {f : ArithmeticFunction R} (hf : f.IsMultiplicative)
(s : Finset ι) (hs : (s : Set ι).Pairwise (Coprime on g)) : f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i) := by
classical
induction s using Finset.induction_on with
| empty => simp [hf]
| insert _ _ has
ih =>
rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
exact Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm
