map_prod_of_prime — Mathlib

English

If f is multiplicative and t consists of primes, then f(∏_{a∈t} a) = ∏_{a∈t} f(a).

Русский

Если f мультипликативна и t состоит из простых, то f(∏_{a∈t} a) = ∏_{a∈t} f(a).

LaTeX

$$$f\left(\prod_{a\in t} a\right) = \prod_{a\in t} f(a)$ при условии, что каждый $a\in t$ является простым$$

Lean4

theorem map_prod_of_prime [CommMonoidWithZero R] {f : ArithmeticFunction R}
    (h_mult : ArithmeticFunction.IsMultiplicative f) (t : Finset ℕ) (ht : ∀ p ∈ t, p.Prime) :
    f (∏ a ∈ t, a) = ∏ a ∈ t, f a :=
  map_prod _ h_mult t fun x hx y hy hxy => (coprime_primes (ht x hx) (ht y hy)).mpr hxy

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