refactor(NumberTheory/LSeries/*): change type of argument to ℕ → ℂ, add LSeries.term + API etc. (#11111)

See [this thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310725.20and.20.2310728.3A.20L-series/near/422590170) on Zulip.

The main point of this PR is to refactor `LSeries` and friends to use an argument `f : ℕ → ℂ` instead of `f : ArithmeticFunction ℂ`. Since I was at it anyway, I also did a few more things:
* Move the L-series stuff out of the `ArithmeticFunction` namespace. Use `LSeries` as a namespace for some of the declarations instead.
* Introduce `LSeries.term f s n`; this denotes the `n`th term in the L-series `LSeries f s`. This is defined to be zero for `n = 0`; otherwise it is the usual `f n / n ^ s`. Provide basic API for it.
* Re-write `LSeries` etc. in terms of `LSeries.term`. Attempt to isolate the meat of the proofs in suitable API lemmas for `LSeries.term`. Add some API (like congruence lemmas).
* Use `s` for the complex variable (in place of `z` or `w`; `s` and `s'` when two are required), following the notational convention in analytic number theory.
* Golf some proofs.
* Add some documentation (and modify existing docstrings to fit the changes).




Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Author: MichaelStollBayreuth