New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(NumberTheory/LSeries/Dirichlet): new file, material on specific L-series #11712
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice work, some (mostly superficial) comments below
LGTM! |
It might be a good idea to apply Ruben's suggestion, changing |
Looks great! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
Thanks! bors merge |
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
Pull request successfully merged into master. Build succeeded: |
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
…L-series (#11712) 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](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837).
This PR adds a new file
NumberTheory.LSeries.Dirichlet
that contains results on L-series of specific functions:1
as a special caseζ
(which has the same L-series as the constant function1
)It also adds (L-series of zero and of the indicator function of
{1}
) and removes (convergence of the L-series of the constant function1
/ ofζ
; this is moved to the new file) some material to/fromNumberTheory.LSeries.Basic
.See this thread on Zulip.