eulerProduct_tprod — Mathlib

English

For a multiplicative arithmetic function f with values in a normed complete ring, the Euler product holds in HasProd form: ∏' p ∑' e f(p^e) = ∑' n f(n).

Русский

Для мультипликативной функций арифметики f со значениями в нормированном полном кольце Эйлерово произведение выполняется в форме HasProd: ∏' p ∑' e f(p^e) = ∑' n f(n).

LaTeX

$$$\\text{HasProd}\\ (p\\mapsto \\sum_{e\\ge0} f(p^e)) (\\sum_{n\\ge0} f(n)).$$$

Lean4

/-- The *Euler Product* for a multiplicative arithmetic function `f` with values in a
complete normed commutative ring `R`: if `‖f ·‖` is summable, then
`∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`. -/
nonrec theorem eulerProduct_tprod {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable (‖f ·‖)) :
    ∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n :=
  eulerProduct_tprod hf.1 hf.2 hsum f.map_zero

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