Theorems · Theorem · number theory

ArithmeticFunction.IsMultiplicative.eulerProduct_tprod

∀ {R : Type u_1} [inst : NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R},
  f.IsMultiplicative → (Summable fun x => ‖f x‖) → ∏' (p : Nat.Primes), ∑' (e : ℕ), f (↑p ^ e) = ∑' (n : ℕ), f n

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.

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

0 results in Mathlib

Foundations

Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingCompleteSpace