English
Let F be a complete normed field. If f: N → F is a completely multiplicative arithmetic function with summable norm, i.e. ∑_{n≥1} ||f(n)|| < ∞, then the Euler product over primes converges and equals the Dirichlet series ∑_{n≥1} f(n): ∑_{n≥1} f(n) = ∏_{p ext{ prime}} (1 − f(p))^{-1}.
Русский
Пусть F — полное нормированное поле. Если f: N → F является полностью мультипликативной арифметической функцией и сумма норм ∑_{n≥1} ||f(n)|| сходится, то Эйлерово произведение по простым числам сходится и равно рядy ∑_{n≥1} f(n): ∑_{n≥1} f(n) = ∏_{p ext{ простое}} (1 − f(p))^{-1}.
LaTeX
$$$\forall f: \mathbb{N} \to F,\; (f(1)=1 \wedge \forall m,n \in \mathbb{N}, f(mn)=f(m)f(n) \wedge \sum_{n=1}^{\infty} \|f(n)\| < \infty) \Rightarrow \sum_{n=1}^{\infty} f(n) = \prod_{p \text{ prime}} (1 - f(p))^{-1}.$$$
Lean4
/-- 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`. -/
theorem eulerProduct_completely_multiplicative_tprod {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
∏' p : Primes, (1 - f p)⁻¹ = ∑' n, f n :=
(eulerProduct_completely_multiplicative_hasProd hsum).tprod_eq
