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): introduce notations #11253
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.
Looks sensible to me
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
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.
Thanks 🎉
bors merge
-/ | ||
|
||
@[inherit_doc] | ||
scoped[LSeries.notation] notation "L" => LSeries |
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.
Will there be a follow-up PR that uses the L
notation in the files in NumberTheory/LSeries/*
? I think it would be good to have that.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
Pull request successfully merged into master. Build succeeded: |
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.
This just introduces
L
as a short notation forLSeries
and↗f
as notation forfun n : ℕ ↦ (f n : ℂ)
,both scoped to
LSeries.notation
. The latter makes it convenient to use arithmetic functionsor Dirichlet characters (or anything that coerces to a function
N → R
, whereℕ
coercesto
N
andR
coerces toℂ
) as arguments toLSeries
etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series.See here on Zulip.