mathlib3 documentation

number_theory.l_series

L-series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an arithmetic function, we define the corresponding L-series.

Main Definitions #

Main Results #

The L-series of an arithmetic_function.

Equations

f.l_series_summable z indicates that the L-series of f converges at z.

Equations