mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat(NumberTheory/LSeries/Dirichlet): new file, material on specific L-series

Open MichaelStollBayreuth opened this issue 1 year ago • 0 comments
trafficstars

This PR adds a new file NumberTheory.LSeries.Dirichlet that contains results on L-series of specific functions:

  • the Möbius function
  • Dirichlet characters, with the constant function 1 as a special case
  • the arithmetic function ζ (which has the same L-series as the constant function 1)
  • the von Mangoldt function and its twists by Dirichlet characters

It also adds (L-series of zero and of the indicator function of {1}) and removes (convergence of the L-series of the constant function 1 / of ζ; this is moved to the new file) some material to/from NumberTheory.LSeries.Basic.

See this thread on Zulip.


Open in Gitpod

MichaelStollBayreuth avatar Mar 26 '24 21:03 MichaelStollBayreuth