Theorems · Theorem · number theory

LSeries_convolution

∀ {f g : ℕ → ℂ} {s : ℂ},
  LSeries.abscissaOfAbsConv f < ↑s.re →
    LSeries.abscissaOfAbsConv g < ↑s.re → LSeries (LSeries.convolution f g) s = LSeries f s * LSeries g s

The L-series of the convolution product f ⍟ g of two sequences f and g equals the product of their L-series in their common half-plane of absolute convergence.

Defined in

Mathlib.NumberTheory.LSeries.Convolution

Cited by

1 results in Mathlib

Foundations

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