English
The L-series of the Dirichlet convolution of two ℂ-valued arithmetic functions f and g equals the product of their L-series, assuming convergence.
Русский
L‑серия свёртки двух ℂ‑значных арифметических функций f и g равна произведению их L‑серий, при условии сходимости.
LaTeX
$$$LSeries (\uparrow (f * g)) s = LSeries (\uparrow f) s \cdot LSeries (\uparrow g) s$$$
Lean4
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
equals the product of their L-series, assuming both L-series converge. -/
theorem LSeries_mul' {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable (↗f) s) (hg : LSeriesSummable (↗g) s) :
LSeries (↗(f * g)) s = LSeries (↗f) s * LSeries (↗g) s :=
coe_mul f g ▸ LSeries_convolution' hf hg
