Theorems · Theorem · number theory

EulerProduct.eulerProduct_completely_multiplicative_hasProd

∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F},
  (Summable fun x => ‖f x‖) → HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)

The Euler Product for completely multiplicative functions. If f : ℕ →*₀ F, where F is a complete normed field and ‖f ·‖ is summable, then ∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n. This version is stated in terms of HasProd.

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldCompleteSpace