L-series

Stream: mathlib4

[Michael Stoll]

I would like to put some part of the code on L-series that I wrote over the last several months into Mathlib.
As a preliminary step, I suggest to create a new directory Mathlib/NumberTheory/LSeries and move the current file Mathlib/NumberTheory/LSeries.lean to Mathlib/NumberTheory/LSeries/Basic.lean. (So that further definitions and results on L-series can go into further files within that directory.)
Are there any objections?

[Johan Commelin]

Sounds good!

[Michael Stoll]

#10385

[Michael Stoll]

After a break (due to travel etc.), I'm now continuing with this sequence of PRs. #10725 is still preliminary; it adds a coercion from R-valued arithmetic functions to complex-valued ones, when ℂ is an R-algebra, so that we can write LSeries ζ or LSeries Λ.

[Michael Stoll]

#10728 now adds some new material: A new predicate LSeriesHasSum and the abscissa of absolute convergence.