map_prod_of_subset_primeFactors — Mathlib

English

If f is multiplicative, and t is a finite set of naturals with t ⊆ l.primeFactors, then f(∏_{a∈t} a) = ∏_{a∈t} f(a).

Русский

Если f мультипликативна, и t — конечное множество натуральных, подмножество primeFactors(l), то f(∏_{a∈t} a) = ∏_{a∈t} f(a).

LaTeX

$$$f\left(\prod_{a\in t} a\right) = \prod_{a\in t} f(a)$ при условии $t \subseteq l\!\text{.primeFactors}$$$

Lean4

theorem map_prod_of_subset_primeFactors [CommMonoidWithZero R] {f : ArithmeticFunction R}
    (h_mult : ArithmeticFunction.IsMultiplicative f) (l : ℕ) (t : Finset ℕ) (ht : t ⊆ l.primeFactors) :
    f (∏ a ∈ t, a) = ∏ a ∈ t, f a :=
  map_prod_of_prime h_mult t fun _ a => prime_of_mem_primeFactors (ht a)

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