-
Notifications
You must be signed in to change notification settings - Fork 297
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(number_theory/legendre_symbol/jacobi_symbol): add new file with the definition and properties of the Jacobi symbol #16395
Conversation
…definition and properties of the Jacobi symbol
The title should be something like feat(number_theory/legendre_symbol/jacobi_symbol): part 1 |
I had edited the title already, but for some reason the change seems to have been lost... |
Since the notation introduced in the file leads to problems with list notation (see the comments near the beginning of |
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.
LGTM, thanks!
bors d+
✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…the definition and properties of the Jacobi symbol (#16395) This PR consists of a new file, `number_theory.legendre_symbol.jacobi_symbol`, that contains a definition of the Jacobi symbol (and sets up notation `[a | b]ⱼ` for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the cases `a = -1`, `a = 2`, `a = -2`, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue class `mod b` and that it depends on `b` only through its residue class `mod 4*a` (quadratic reciprocity is needed for the latter). The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code). Discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984)
Pull request successfully merged into master. Build succeeded: |
…the definition and properties of the Jacobi symbol (#16395) This PR consists of a new file, `number_theory.legendre_symbol.jacobi_symbol`, that contains a definition of the Jacobi symbol (and sets up notation `[a | b]ⱼ` for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the cases `a = -1`, `a = 2`, `a = -2`, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue class `mod b` and that it depends on `b` only through its residue class `mod 4*a` (quadratic reciprocity is needed for the latter). The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code). Discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984)
…ym* to other namespaces (#16461) This PR moves `legendre_sym` and `jacobi_sym` (and `qr_sign`) to the root namespace. It also moves definitions and lemmas named `legendre_sym_...` to the `legendre_sym` namespace and analogous for `jacobi_sym_...` and `qr_sign_...`. We change names like `jacobi_sym_two` to `jacobi_sym.at_two`. This mostly affects the files `number_theory.legendre_symbol.quadratic_reciprocity` and `number_theory.legendre_symbol.jacobi_symbol`. Note that names like `exists_sq_eq_neg_one_iff` have been left in `zmod`. We prefix `quadratic_reciprocity*` by `legendre_sym` to disambiguate with the versions for the Jacobi symbol. (The links in `docs/100.yaml` and `docs/overview.yaml` are updated accordingly.) We also move the results in `number_theory.legendre_symbol.gauss_eisenstein_lemmas` from the `legendre_symbol` namespace to the `zmod` namespace. See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/297792676) and the comments at [#16395](#16395) for discussion.
…the definition and properties of the Jacobi symbol (#16395) This PR consists of a new file, `number_theory.legendre_symbol.jacobi_symbol`, that contains a definition of the Jacobi symbol (and sets up notation `[a | b]ⱼ` for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the cases `a = -1`, `a = 2`, `a = -2`, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue class `mod b` and that it depends on `b` only through its residue class `mod 4*a` (quadratic reciprocity is needed for the latter). The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code). Discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984)
…ym* to other namespaces (#16461) This PR moves `legendre_sym` and `jacobi_sym` (and `qr_sign`) to the root namespace. It also moves definitions and lemmas named `legendre_sym_...` to the `legendre_sym` namespace and analogous for `jacobi_sym_...` and `qr_sign_...`. We change names like `jacobi_sym_two` to `jacobi_sym.at_two`. This mostly affects the files `number_theory.legendre_symbol.quadratic_reciprocity` and `number_theory.legendre_symbol.jacobi_symbol`. Note that names like `exists_sq_eq_neg_one_iff` have been left in `zmod`. We prefix `quadratic_reciprocity*` by `legendre_sym` to disambiguate with the versions for the Jacobi symbol. (The links in `docs/100.yaml` and `docs/overview.yaml` are updated accordingly.) We also move the results in `number_theory.legendre_symbol.gauss_eisenstein_lemmas` from the `legendre_symbol` namespace to the `zmod` namespace. See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/297792676) and the comments at [#16395](#16395) for discussion.
This PR consists of a new file,
number_theory.legendre_symbol.jacobi_symbol
, that contains a definition of the Jacobi symbol (and sets up notation[a | b]ⱼ
for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the casesa = -1
,a = 2
,a = -2
, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue classmod b
and that it depends onb
only through its residue classmod 4*a
(quadratic reciprocity is needed for the latter).The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code).
Discussion on Zulip