mathlib3

9500d951 - feat(number_theory/l_series): The L-series of an arithmetic function (#7862)

feat(number_theory/l_series): The L-series of an arithmetic function (#7862) Defines the L-series of an arithmetic function Proves a few basic facts about convergence of L-series