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/quadratic_reciprocity): change order of arguments … #13311
Conversation
@@ -356,13 +360,13 @@ namespace zmod | |||
* `-1` otherwise. | |||
|
|||
-/ | |||
def legendre_sym (a : ℤ) (p : ℕ) : ℤ := | |||
def legendre_sym (p : ℕ) (a : ℤ) : ℤ := |
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.
Please also include a warning about the order of the arguments in the docstring. (I saw you already added that warning above in the module docs.)
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; I had overlooked that. I have changed the docstring accordingly.
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
#13311) …in legendre_sym This is the first step in a major overhaul of the contents of number_theory/quadratic_reciprocity. As a first step, the order of the arguments `a` and `p` to `legendre_sym` is swapped, based on a [poll](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Quadratic.20Hilbert.20symbol.20over.20.E2.84.9A) on Zulip.
Pull request successfully merged into master. Build succeeded: |
…in legendre_sym
This is the first step in a major overhaul of the contents of number_theory/quadratic_reciprocity.
As a first step, the order of the arguments
a
andp
tolegendre_sym
is swapped, based on a poll on Zulip.