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 type of a
in API lemmas to int
#13393
Conversation
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…emmas to `int` (#13393) This is step 2 in the overhaul of number_theory/qudratic_reciprocity. The only changes are that the argument `a` is now of type `int` rather than `nat` in a bunch of statements. This is more natural, since the corresponding (now second) argument of `legendre_symnbol` is of type `int`; it therefore makes the API lemmas more easily useable.
legendre_sym p a = 1 ↔ (∃ b : zmod p, b ^ 2 = a) := | ||
begin | ||
rw [euler_criterion p ha0, legendre_sym, int.cast_coe_nat, if_neg ha0], | ||
rw [euler_criterion p ha0, legendre_sym, if_neg ha0], | ||
split_ifs, | ||
{ simp only [h, eq_self_iff_true] }, | ||
{ simp only [h, iff_false], tauto } | ||
end | ||
|
||
lemma eisenstein_lemma [fact (p % 2 = 1)] {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : zmod p) ≠ 0) : |
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.
Should this become an integer too?
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.
I have left this, since the proof does not seem to be easily adaptable. The result is used for proving quadratic reciprocity, wheere the arguments are (natural) prime numbers, and there is probably not much use outside of this.
a
in API lemmas to int
a
in API lemmas to int
Pull request successfully merged into master. Build succeeded: |
a
in API lemmas to int
a
in API lemmas to int
This is step 2 in the overhaul of
number_theory/quadratic_reciprocity
.The only changes are that the argument
a
is now of typeint
rather thannat
in a bunch of statements.This is more natural, since the corresponding (now second) argument of
legendre_symnbol
is of typeint
; it therefore makes the API lemmas more easily useable.