prodPrimeFactors — Mathlib

English

Given a function f: ℕ → R, define prodPrimeFactors f by (prodPrimeFactors f)(n) = 0 if n = 0, and ∏_{p ∈ n.primeFactors} f(p) otherwise.

Русский

Для функции f: ℕ → R определяем prodPrimeFactors f таким образом: (prodPrimeFactors f)(n) = 0 при n = 0, иначе ∏_{p ∈ primeFactors(n)} f(p).

LaTeX

$$$$ (prodPrimeFactors\; f)(n) = \begin{cases} 0, & n = 0, \\ \prod_{p \in n.primeFactors} f(p), & n \neq 0. \end{cases} $$$$

Lean4

/-- The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function -/
def prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) : ArithmeticFunction R
    where
  toFun d := if d = 0 then 0 else ∏ p ∈ d.primeFactors, f p
  map_zero' := if_pos rfl

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