English
The L-series of the Dirichlet convolution of two ℂ-valued arithmetic functions f and g equals the product of their L-series in the abscissa region where both converge.
Русский
L‑серия свёртки двух ℂ‑значных арифметических функций f и g равна произведению их L‑серий в области абсцисс сходимости обеих серий.
LaTeX
$$$abscissaOfAbsConv (\uparrow f) < s.re \land abscissaOfAbsConv (\uparrow g) < s.re \Rightarrow 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 in their common half-plane of absolute convergence. -/
theorem LSeries_mul {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : abscissaOfAbsConv ↗f < s.re)
(hg : abscissaOfAbsConv ↗g < s.re) : LSeries (↗(f * g)) s = LSeries (↗f) s * LSeries (↗g) s :=
coe_mul f g ▸ LSeries_convolution hf hg
